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

Goal state before:
pp: case case
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s s' : Option Γ'
h :
  Reaches₁ (TM2.step tr) { l := some (Λ'.pred ?m.739 ?m.740), var := s, stk := elim (trList v) [] ?m.741 ?m.742 }
    (Nat.rec { l := some ?m.739, var := s', stk := elim (trList v.tail) [] ?m.741 ?m.742 }
      (fun n x ↦ { l := some ?m.740, var := s', stk := elim (trList (n :: v.tail)) [] ?m.741 ?m.742 }) v.headI)
⊢ ∃ b₂,
    TrCfg (Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) v.headI) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
revert h

Goal state after:
case case
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s s' : Option Γ'
⊢ Reaches₁ (TM2.step tr) { l := some (Λ'.pred ?m.739 ?m.740), var := s, stk := elim (trList v) [] ?m.741 ?m.742 }
      (Nat.rec { l := some ?m.739, var := s', stk := elim (trList v.tail) [] ?m.741 ?m.742 }
        (fun n x ↦ { l := some ?m.740, var := s', stk := elim (trList (n :: v.tail)) [] ?m.741 ?m.742 }) v.headI) →
    ∃ b₂,
      TrCfg (Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) v.headI) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case empty
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
S : Set (Set ↑(F.obj j))
⊢ ∀ (P : J → Set ↑(F.obj j)),
    Set.univ ∈ S → (∀ (A B : Set ↑(F.obj j)), A ∈ S → B ∈ S → A ∩ B ∈ S) → (∀ e ∈ ∅, P e ∈ S) → ⋂ e ∈ ∅, P e ∈ S

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_3.mpr.refine_2
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
e : J
he : e ∈ G
⊢ (fun x ↦ (ConcreteCategory.hom (C.π.app e)) x) ⁻¹' U e = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' Vs e

Tactic:
simp [Vs, dif_pos he, ← Set.preimage_comp, ← coe_comp]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Yoneda

Goal state before:
pp: Y : Type w'
inst✝ : TopologicalSpace Y
α : Type
X : α → TopCat
⊢ (piComparison (yonedaPresheaf' Y) fun x ↦ op (X x)) =
    (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:
rw [← Category.assoc, Iso.eq_comp_inv]
  ext
  simp [yonedaPresheaf', piComparison, ← opCoproductIsoProduct_inv_comp_ι]
  rfl

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

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ (functorOp c).Final

Tactic:
by
  have := functor_initial c hc
  have : ((StructuredArrow.toCostructuredArrow toLightProfinite c.pt)).IsEquivalence :=
    (inferInstance : (structuredArrowOpEquivalence _ _).functor.IsEquivalence)
  have : (functor c).rightOp.Final :=
    inferInstanceAs ((opOpEquivalence ℕ).inverse ⋙ (functor c).op).Final
  exact Functor.final_comp (functor c).rightOp _

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

Goal state before:
pp: X✝ Y✝ : LightProfinite
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi (lightProfiniteToLightCondSet.map f)

Tactic:
LightCondSet.epi_iff_locallySurjective_on_lightProfinite

Goal state after:
X✝ Y✝ : LightProfinite
f : X✝ ⟶ Y✝
hf : Epi f
⊢ ∀ (S : LightProfinite) (y : (lightProfiniteToLightCondSet.obj Y✝).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom ((lightProfiniteToLightCondSet.map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom ((lightProfiniteToLightCondSet.obj Y✝).obj.map (Opposite.op φ))) y
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
this : Finite ↑(fiber f x).toTop
y : ↑(fiber f x).toTop
⊢ (ConcreteCategory.hom (isoFinYonedaComponents X (fiber f x)).hom)
      ((ConcreteCategory.hom (X.map (sigmaIncl f x).op))
        ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f))
      y =
    (ConcreteCategory.hom (isoFinYonedaComponents X (fiber f x)).hom)
      ((ConcreteCategory.hom (X.map (CompHausLike.isTerminalPUnit.from (fiber f x)).op)) (Function.Fiber.image (⇑f) x))
      y

Tactic:
simp only [toProfinite_obj, isoFinYonedaComponents_hom, ConcreteCategory.hom_ofHom,
    TypeCat.Fun.coe_mk, ← Functor.map_comp_apply, ← op_comp]

Goal state after:
case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
this : Finite ↑(fiber f x).toTop
y : ↑(fiber f x).toTop
⊢ (ConcreteCategory.hom (X.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) y ≫ sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom
        (X.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) y ≫ CompHausLike.isTerminalPUnit.from (fiber f x)).op))
      (Function.Fiber.image (⇑f) x)
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 : Epi ((LightCondensed.forget R).map f)
⊢ ∃ T π g, Epi π ∧ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p = g ≫ f

Tactic:
LightCondSet.epi_iff_locallySurjective_on_lightProfinite

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 π g, Epi π ∧ (lightProfiniteToLightCondSet ⋙ LightCondensed.free R).map π ≫ p = g ≫ f
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case e_6
R : Type u
inst✝ : CommRing R
A B P : LightCondMod R
S : LightProfinite
e : A ⟶ B
x : ↑((P ⟹ A).obj.obj (Opposite.op S))
⊢ (coherentTopology LightProfinite).yonedaEquiv.symm
      ((ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S))) x) =
    (coherentTopology LightProfinite).yonedaEquiv.symm x ≫ (forget R).map ((ihom P).map e)

Tactic:
apply (coherentTopology LightProfinite.{u}).yonedaEquiv.injective

Goal state after:
case e_6
R : Type u
inst✝ : CommRing R
A B P : LightCondMod R
S : LightProfinite
e : A ⟶ B
x : ↑((P ⟹ A).obj.obj (Opposite.op S))
⊢ (coherentTopology LightProfinite).yonedaEquiv
      ((coherentTopology LightProfinite).yonedaEquiv.symm
        ((ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S))) x)) =
    (coherentTopology LightProfinite).yonedaEquiv
      ((coherentTopology LightProfinite).yonedaEquiv.symm x ≫ (forget R).map ((ihom P).map e))
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
h_glue : ∀ (i j : S), ∀ x ∈ C i, x ∈ C j → i = j
⊢ IsLocallyConstant (liftCover C (fun i x ↦ i) h_glue C_cover_univ)

Tactic:
rw [IsLocallyConstant.iff_isOpen_fiber]

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
h_glue : ∀ (i j : S), ∀ x ∈ C i, x ∈ C j → i = j
⊢ ∀ (y : S), IsOpen[inst✝⁸] (liftCover C (fun i x ↦ i) h_glue C_cover_univ ⁻¹' {y})
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
x : t (F (G α))
⊢ traverse Comp.mk x = traverse (Comp.mk ∘ map id ∘ id) x

Tactic:
simp [map_id]

Goal state after:
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
inst✝ : Traversable t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
h₂ :
  ∀ {F : Type u → Type u} [inst : Applicative F] [LawfulApplicative F] {α β : Type u} (f : α → F β),
    traverse f = Equiv.traverse eqv f
α✝ : Type u
x✝ : t' α✝
⊢ traverse pure x✝ = pure x✝

Tactic:
rw [h₂, Equiv.id_traverse]

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: case succ
z : ℤ
n✝ : ℕ
⊢ { toFin := ↑z } = ↑z

Tactic:
case succ w =>
    apply BitVec.eq_of_toInt_eq
    rw [toInt_ofFin, Fin.val_intCast, Int.natCast_pow, Nat.cast_ofNat, Int.ofNat_toNat,
      toInt_intCast]
    rw [Int.max_eq_left]
    · have h : (2 ^ (w + 1) : Int) = (2 ^ (w + 1) : Nat) := by simp
      rw [h, Int.emod_bmod]
    · omega

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toDFinsupp (s ∩ t) = toDFinsupp s ⊓ toDFinsupp t

Tactic:
ext i; simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toDFinsupp (s ∪ t) = toDFinsupp s ⊔ toDFinsupp t

Tactic:
ext i; simp

Goal state after:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: case empty
ι : Type u_2
α : Type u_3
f : ι → α → ℕ∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
⊢ ⨅ i, ∑ a ∈ ∅, f i a = ∑ a ∈ ∅, ⨅ i, f i a

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: case empty
α : Type u_1
ι : Type u_2
f : α → ι → ℕ∞
hf : ∀ (i j : ι), ∃ k, ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k
⊢ ∑ a ∈ ∅, ⨆ i, f a i = ⨆ i, ∑ a ∈ ∅, f a i

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Data.Semiquot

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

Tactic:
revert h

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

Goal state before:
pp: α✝ : Type u
β✝ : α✝ → Type v
α : Type ?u.19
β : Type ?u.20
f : α → β
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Injective f
⊢ ∀ (x : α), x ∈ List.filterMap (partialInv f) (toList β)

Tactic:
intro x
      simp only [mem_toList, true_and, List.mem_filterMap]
      use f x
      simp only [h, Function.partialInv_left]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
⊢ (insert a b (singleton a b')).entries = (singleton a b).entries

Tactic:
by
    simp only [AList.entries_insert, List.kerase_cons_eq, AList.singleton_entries]

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

Goal state before:
pp: case swap.some.some
α : 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)
c : α
h₁ : f a = some c
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
rcases (pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) _ h₂ _ h₁ with ⟨rfl, rfl⟩

Goal state after:
case swap.some.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
b : α
l : List α
d : α
h₂ : f b = some d
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: b :: l)
h₁ : f b = some d
⊢ lookmap f (b :: b :: l) ~ lookmap f (b :: b :: l)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
l : List α
⊢ (map Prod.snd l.zipIdx).Nodup

Tactic:
simp [List.nodup_range']

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
a : α
⊢ dlookup a (l₁ ++ l₂) = (dlookup a l₁).or (dlookup a l₂)

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

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : t.Nonempty
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
exact let ⟨p, hp⟩ := exists_lt (t.min' ht); ⟨p, by simp_all⟩

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (lookupAll a l).Nodup

Tactic:
by
  (rw [lookupAll_eq_dlookup a h]; apply Option.toList_nodup)

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: case empty
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
⊢ (∅.inf fun i ↦ (t i).sup (f i)) = (∅.pi t).sup fun g ↦ ∅.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)

Tactic:
| empty =>

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : Sigma β
xs : List (Sigma β)
h : sizeOf xs.dedupKeys ≤ sizeOf xs
⊢ sizeOf (x :: kerase x.fst xs.dedupKeys) ≤ sizeOf (x :: xs)

Tactic:
exact sizeOf_cons_le_sizeOf_cons x (le_trans (sizeOf_kerase x.fst xs.dedupKeys) h)

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
this : _root_.Disjoint hd.support (foldr (fun x y ↦ x.support ⊔ y) ∅ tl)
⊢ _root_.Disjoint hd.support tl.sum.support

Tactic:
exact Finset.disjoint_of_subset_right (List.support_sum_subset _) this

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝ : Mul α
x : Holor α []
y : Holor α ds
⊢ x ⊗ y = x ⟨[], ⋯⟩ • y

Tactic:
by
  simp +unfoldPartialApp [mul, SMul.smul, HolorIndex.take, HolorIndex.drop,
    HSMul.hSMul]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : Add α
i : ℕ
hid : i < d
x y : Holor α (d :: ds)
t : HolorIndex ds
⊢ (x.slice i hid + y.slice i hid) t = (x + y).slice i hid t

Tactic:
by simp [slice, (· + ·), Add.add]

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑b - ↑(v % r)) / ↑r⌉

Tactic:
← div_add_mod b r,

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑(r * (b / r) + b % r) - ↑(v % r)) / ↑r⌉
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
⊢ l.rtake n = (take n l.reverse).reverse

Tactic:
rtake

Goal state after:
α : Type u_1
l : List α
n : ℕ
⊢ drop (l.length - n) l = (take n l.reverse).reverse
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : (head :: tail).sum ≤ l.length
⊢ map length ((head :: tail).splitLengths l) = head :: tail

Tactic:
simp only [sum_cons] at h
    simp only [splitLengths_cons, map_cons, length_take, cons.injEq, min_eq_left_iff]
    rw [ih]
    · simp [Nat.le_of_add_right_le h]
    · simp [Nat.le_sub_of_add_le' h]

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

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
shift_position' : (u ++ (v ++ w))[j + u.length + p]? = v[j + p]?
⊢ v[j]? = v[j + p]?

Tactic:
have : ∀ i < u.length + (v.length + w.length) - p,
      (u ++ (v ++ w))[i]? = (u ++ (v ++ w))[i + p]? := by
    simp_all [hasPeriod_iff_getElem?]

Goal state after:
α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
shift_position' : (u ++ (v ++ w))[j + u.length + p]? = v[j + p]?
this : ∀ i < u.length + (v.length + w.length) - p, (u ++ (v ++ w))[i]? = (u ++ (v ++ w))[i + p]?
⊢ v[j]? = v[j + p]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬([] = a ∨ [] ∈ l)
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' : IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (a :: l)
⊢ splitBy r (a :: l).flatten = a :: l

Tactic:
not_or,

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬[] = a ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' : IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (a :: l)
⊢ splitBy r (a :: l).flatten = a :: l
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case intro.intro.inr.empty
α : Type u_1
inst✝ : Preorder α
a✝ a : α
h✝ : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M✝ M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
hN : ∀ (x : α), x ∈ 0 → x < a
⊢ Acc OneStep (M + 0)

Tactic:
| empty =>

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

Goal state before:
pp: case empty
α : Type u_1
inst✝ : Preorder α
M : Multiset α
hM : ∀ (x : α), x ∈ 0 → Acc LT.lt x
⊢ Acc OneStep 0

Tactic:
| empty =>

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:
| empty =>

Goal state after:
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
hlp : (List.map s l).prod = (List.map s l').prod
⊢ ∀ i ∈ l', s i ≠ 0

Tactic:
simpa [List.Perm.mem_iff hl.symm] using hs

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a n : ℕ
⊢ n.ceilRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0

Tactic:
by
  simp +contextual [ceilRoot_def, not_or]

Goal state after: