mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Stonean.Basic

Goal state before:
pp: X Y : Stonean
f : X ⟶ Y
h : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
⊢ False

Tactic:
have hC : IsClosed C := (isCompact_range f.hom.hom.continuous).isClosed

Goal state after:
X Y : Stonean
f : X ⟶ Y
h : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
⊢ False
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
⊢ ∀ (i j : J) (f : i ⟶ j),
    ∀ V ∈ {W | IsClopen W}, ⇑(ConcreteCategory.hom ((F ⋙ toTopCat).map f)) ⁻¹' V ∈ {W | IsClopen W}

Tactic:
rintro i j f V (hV : IsClopen _)

Goal state after:
case refine_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
i j : J
f : i ⟶ j
V : Set ↑((F ⋙ toTopCat).obj j)
hV : IsClopen V
⊢ ⇑(ConcreteCategory.hom ((F ⋙ toTopCat).map f)) ⁻¹' V ∈ {W | IsClopen W}
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: case mp
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
⊢ False

Tactic:
have hC : IsClosed C := (isCompact_range f.hom.hom.continuous).isClosed

Goal state after:
case mp
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
⊢ False
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: case mpr
X Y : LightProfinite
f : X ⟶ Y
⊢ Epi (↾⇑(ConcreteCategory.hom f)) → Epi f

Tactic:
apply (forget LightProfinite).epi_of_epi_map

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

Goal state before:
pp: J : Type v
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toTop) (α → Fin 2)
h : LocallyConstant.map (fun a b ↦ if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
let ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
  let σ : (α → Fin 2) → α := fun f => if h : ∃ a : α, ι a = f then h.choose else default
  refine ⟨j, gg.map σ, ?_⟩
  ext x
  simp only [LocallyConstant.coe_comap, LocallyConstant.map_apply,
    Function.comp_apply]
  dsimp [σ]
  have h1 : ι (f x) = gg (C.π.app j x) := by
    change f.map (fun a b => if a = b then (0 : Fin 2) else 1) x = _
    rw [h]
    rfl
  have h2 : ∃ a : α, ι a = gg (C.π.app j x) := ⟨f x, h1⟩
  rw [dif_pos]
  swap
  · assumption
  apply_fun ι
  · rw [h2.choose_spec]
    exact h1
  · intro a b hh
    have hhh := congr_fun hh a
    dsimp [ι] at hhh
    rw [if_pos rfl] at hhh
    split_ifs at hhh with hh1
    · exact hh1.symm
    · exact False.elim (bot_ne_top hhh)

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

Goal state before:
pp: case inl
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
suffices ∃ j, IsEmpty (F.obj j) by
      refine this.imp fun j hj => ?_
      refine ⟨⟨hj.elim, fun A => ?_⟩, ?_⟩
      · convert! isOpen_empty
        ext x
        exact hj.elim x
      · ext x
        exact hj.elim' (C.π.app j x)
    by_contra! h
    have : ∀ j : J, Nonempty ((F ⋙ Profinite.toTopCat).obj j) := h
    have : ∀ j : J, T2Space ((F ⋙ Profinite.toTopCat).obj j) := fun j =>
      (inferInstance : T2Space (F.obj j))
    have : ∀ j : J, CompactSpace ((F ⋙ Profinite.toTopCat).obj j) := fun j =>
      (inferInstance : CompactSpace (F.obj j))
    have cond := TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system.{u}
      (F ⋙ Profinite.toTopCat)
    suffices Nonempty C.pt from IsEmpty.false (S.proj this.some)
    let D := Profinite.toTopCat.mapCone C
    have hD : IsLimit D := isLimitOfPreserves Profinite.toTopCat hC
    have CD := (hD.conePointUniqueUpToIso (TopCat.limitConeIsLimit.{v, max u v} _)).inv
    exact cond.map CD

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

Goal state before:
pp: X : CondensedSet
h : (S : Profinite) → IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op)
⊢ LocallyConstant.functor.essImage X

Tactic:
let e : CondensedSet.{u} ≌ Sheaf (coherentTopology Profinite) _ :=
    (Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).symm
  let i : (e.functor.obj X).obj ≅ (e.functor.obj (LocallyConstant.functor.obj _)).obj :=
    Condensed.isoLocallyConstantOfIsColimit _ h
  exact ⟨_, ⟨e.functor.preimageIso ((sheafToPresheaf _ _).preimageIso i.symm)⟩⟩

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

Goal state before:
pp: 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)
⊢ univ.PairwiseDisjoint Z

Tactic:
Set.pairwiseDisjoint_iff

Goal state after:
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)
⊢ ∀ ⦃i : S⦄, i ∈ univ → ∀ ⦃j : S⦄, j ∈ univ → (Z i ∩ Z j).Nonempty → i = j
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: 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
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ i = j

Tactic:
Set.pairwiseDisjoint_iff

Goal state after:
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 : ∀ ⦃i : S⦄, i ∈ univ → ∀ ⦃j : S⦄, j ∈ univ → (C i ∩ C j).Nonempty → i = j
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
i j : S
x : Y
hxi : x ∈ C i
hxj : x ∈ C j
⊢ i = j
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: case refine_2
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 : Y
hy : y ∈ ⋃ i, C i
⊢ (f' ∘ liftCover C (fun i x ↦ i) h_glue C_cover_univ) y = g' y

Tactic:
obtain ⟨i, hi⟩ := mem_iUnion.mp hy

Goal state after:
case refine_2
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 : Y
hy : y ∈ ⋃ i, C i
i : S
hi : y ∈ C i
⊢ (f' ∘ liftCover C (fun i x ↦ i) h_glue C_cover_univ) y = g' 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 α))
⊢ sequence (Comp.mk <$> x) = Comp.mk (sequence <$> sequence x)

Tactic:
by
  simp only [sequence, traverse_map, id_comp]; rw [← comp_traverse]; simp [map_id]

Goal state after:
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
z : Upto p
⊢ p (k + ↑z) → Nat.find h' = k + ↑z → ⋯.fix (fixAux f) z x = Fix.approx f (k + 1) x

Tactic:
intro _this hk

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
hk : Nat.find h' = k + ↑z
⊢ ⋯.fix (fixAux f) z x = Fix.approx f (k + 1) x
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // ofRepeat (α.PredLast' pp i p_1) }) i.fs
⊢ ofRepeat (α.PredLast' pp i.fs ↑x) = α.PredLast pp ↑x

Tactic:
grind [PredLast]

Goal state after:
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: case mk.e_map
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³ → x✝²
x✝ : t' x✝³
⊢ map✝ x✝¹ x✝ = Equiv.map eqv x✝¹ x✝

Tactic:
← h₀

Goal state after:
case mk.e_map
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³ → x✝²
x✝ : t' x✝³
⊢ map✝ x✝¹ x✝ = x✝¹ <$> x✝
Module: Mathlib.Data.BitVec

Goal state before:
pp: z : ℤ
w : ℕ
⊢ 0 ≤ z % 2 ^ (w + 1)

Tactic:
omega

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : f.Realizer
x : F.σ
h : f ≠ ⊥
hF : F.F.f x ⊆ ∅
⊢ f = ⊥

Tactic:
rw [← F.eq, eq_bot_iff]

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : TopologicalSpace α
f : Filter α
F : f.Realizer
x : F.σ
h : f ≠ ⊥
hF : F.F.f x ⊆ ∅
⊢ F.F.toFilter ≤ ⊥
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
⊢ (List.take m l).get = take m h l.get ∘ Fin.cast ⋯

Tactic:
ext i
  simp only [List.get_eq_getElem, List.getElem_take, comp_apply, take_apply, val_castLE, val_cast]

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ map (Sigma.mk a) (lookupAll a (⟨a, b'⟩ :: l)) <+ ⟨a, b'⟩ :: l

Tactic:
simp only [lookupAll_cons_eq, List.map]

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ ⟨a, b'⟩ :: map (Sigma.mk a) (lookupAll a l) <+ ⟨a, b'⟩ :: l
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
⊢ Multiset α' → F (Multiset β')

Tactic:
by
  refine Quotient.lift (Functor.map ofList ∘ Traversable.traverse f) ?_
  introv p; unfold Function.comp
  induction p with
  | nil => rfl
  | @cons x l₁ l₂ _ h =>
    have :
      Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₁ =
        Multiset.cons <$> f x <*> ofList <$> Traversable.traverse f l₂ := by
      rw [h]
    simpa [functor_norm] using! this
  | swap x y l =>
    have :
      (fun a b (l : List β') ↦ (↑(a :: b :: l) : Multiset β')) <$> f y <*> f x =
        (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y := by
      rw [CommApplicative.commutative_map]
      congr 2
      funext a b l
      simpa [flip] using! Perm.swap a b l
    simp [Function.comp_def, this, functor_norm]
  | trans => simp [*]

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

Goal state before:
pp: α β : Type u_1
h : α → β
⊢ Functor.map h ∘ ofList = ofList ∘ Functor.map h

Tactic:
funext; simp only [Function.comp_apply, fmap_def, map_coe, List.map_eq_map]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ (x ⊗ y ⊗ z) t = (x ⊗ (y ⊗ z)).assocLeft t

Tactic:
assocLeft

Goal state after:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ (x ⊗ y ⊗ z) t = cast ⋯ (x ⊗ (y ⊗ z)) t
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (i :: is) (d :: ds)

Tactic:
rw [← h]; exact t.2

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : a✝ ∉ s✝
ih : ∑ x ∈ s✝, (f x).slice i hid = (∑ x ∈ s✝, f x).slice i hid
⊢ ∑ x ∈ insert a✝ s✝, (f x).slice i hid = (∑ x ∈ insert a✝ s✝, f x).slice i hid

Tactic:
rw [Finset.sum_insert h_not_in, ih, slice_add, Finset.sum_insert h_not_in]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α []
h : CPRankMax (0 + 1) x
⊢ CPRankMax 1 x

Tactic:
zero_add

Goal state after:
α : Type
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α []
h : CPRankMax 1 x
⊢ CPRankMax 1 x
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case false
n : ℕ
⊢ -[2 * n.div2+1] = -[0 + 2 * n.div2+1]

Tactic:
zero_add

Goal state after:
case false
n : ℕ
⊢ -[2 * n.div2+1] = -[2 * n.div2+1]
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ (y₁ + y₂))

Tactic:
rw [mul_left_distrib]

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ y₁ + x ⊗ y₂)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b -[n+1]).testBit 0 = b

Tactic:
rw [bit_negSucc]; dsimp [testBit]; rw [Nat.testBit_bit_zero, Bool.not_not]

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

Goal state before:
pp: b : Bool
n : ℤ
⊢ 0 + n = n

pp: b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 = 0

pp: case H
b : Bool
n : ℤ
⊢ 2 ≠ 0

Tactic:
zero_add

Goal state after:
b : Bool
n : ℤ
⊢ n = n

b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 = 0

case H
b : Bool
n : ℤ
⊢ 2 ≠ 0
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v : ℕ
x : ℤ
h : (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
⊢ 0 ≤ x

Tactic:
omega

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
by
  induction l with
  | nil => simp [dropWhile]
  | cons x xs IH => by_cases hp : p x <;> simp [hp, IH]

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

Goal state before:
pp: case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : true = p head
⊢ find? p (head :: tail) = (dropWhile (fun x ↦ !p x) (head :: tail)).head?

Tactic:
rw [find?_cons_of_pos phh.symm, dropWhile_cons_of_neg]

Goal state after:
case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : true = p head
⊢ some head = (head :: tail).head?

case true
α : Type u_1
p : α → Bool
l : List α
head : α
tail : List α
hi : find? p tail = (dropWhile (fun x ↦ !p x) tail).head?
phh : true = p head
⊢ ¬(!p head) = true
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case neg
n m : ℕ
h : m ≤ n
⊢ IsChain (fun a b ↦ b = a.succ) (Ico n m)

Tactic:
rw [eq_nil_of_le h]

Goal state after:
case neg
n m : ℕ
h : m ≤ n
⊢ IsChain (fun a b ↦ b = a.succ) []
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case inr.inr
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
⊢ (take n w ++ w).HasPeriod p

Tactic:
hasPeriod_iff_forall_getElem?_mod

Goal state after:
case inr.inr
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
⊢ ∀ i < (take n w ++ w).length, (take n w ++ w)[i]? = (take n w ++ w)[i % p]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case mpr
α : Type u_1
m : List α
r : α → α → Bool
l : List (List α)
⊢ m = l.flatten ∧
      ¬[] ∈ 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 m = l

Tactic:
rintro ⟨rfl, hn, hc, hc'⟩

Goal state after:
case mpr
α : Type u_1
r : α → α → Bool
l : List (List α)
hn : ¬[] ∈ l
hc : ∀ (m : List α), m ∈ 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) l
⊢ splitBy r l.flatten = l
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N P : Multiset α
⊢ M.IsDershowitzMannaLT N → N.IsDershowitzMannaLT P → M.IsDershowitzMannaLT P

Tactic:
rintro ⟨X₁, Y₁, Z₁, -, rfl, rfl, hYZ₁⟩ ⟨X₂, Y₂, Z₂, hZ₂, hXZXY, rfl, hYZ₂⟩

Goal state after:
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : X₁ + Z₁ = X₂ + Y₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case cons
α : 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
⊢ TransGen OneStep M N

Tactic:
| cons z Z ih =>

Goal state after:
case cons
α : 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
⊢ TransGen OneStep M N
Module: Mathlib.Data.Nat.Cast.SetInterval

Goal state before:
pp: a : ℕ
⊢ Nat.cast '' Iic a = Icc 0 ↑a

Tactic:
by
  rw [← Icc_bot, image_cast_int_Icc]; rfl

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

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ ↑n.properDivisors = {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

Tactic:
refine Set.ext fun k ↦ ⟨fun h ↦ ?_, fun ⟨f, hlt, h⟩ ↦ ?_⟩

Goal state after:
case neg.refine_1
n : ℕ
hn : ¬n = 0
k : ℕ
h : k ∈ ↑n.properDivisors
⊢ k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}

case neg.refine_2
n : ℕ
hn : ¬n = 0
k : ℕ
x✝ : k ∈ {x | ∃ f < n.factorization, (f.prod fun x1 x2 ↦ x1 ^ x2) = x}
f : ℕ →₀ ℕ
hlt : f < n.factorization
h : (f.prod fun x1 x2 ↦ x1 ^ x2) = k
⊢ k ∈ ↑n.properDivisors