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

Goal state before:
pp: case mp
X Y : Profinite
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
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
⊢ False

Tactic:
obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_isClopen.mem_nhds_iff.mp hUy

Goal state after:
case mp
X Y : Profinite
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
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
⊢ False
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)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hUy : U ∈ 𝓝 y
⊢ False

Tactic:
obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_isClopen.mem_nhds_iff.mp hUy

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
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
⊢ False
Module: Mathlib.Topology.ClopenBox

Goal state before:
pp: case refine_1
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
⊢ {s | IsClopen s}.Countable

Tactic:
let f : {s : Set X | IsClopen s} → Clopens X := fun s ↦ ⟨s.1, s.2⟩

Goal state after:
case refine_1
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : TotallyDisconnectedSpace X
h : Countable (Clopens X)
f : ↑{s | IsClopen s} → Clopens X := fun s ↦ { carrier := ↑s, isClopen' := ⋯ }
⊢ {s | IsClopen s}.Countable
Module: Mathlib.Condensed.Light.Basic

Goal state before:
pp: C : Type w
inst✝ : Category.{v, w} C
X Y : LightCondensed C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S
⊢ f = g

Tactic:
apply Sheaf.hom_ext

Goal state after:
C : Type w
inst✝ : Category.{v, w} C
X Y : LightCondensed C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S
⊢ f.hom = g.hom
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)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
⊢ False

Tactic:
obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_isClopen.mem_nhds_iff.mp hUy

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
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
⊢ False
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: S : Finset Λ'
k : Cont'
H₁ : contSupp k ⊆ S
⊢ TM2.SupportsStmt S (tr (Λ'.ret k))

Tactic:
have W := fun {q} => trStmts₁_self q

Goal state after:
S : Finset Λ'
k : Cont'
H₁ : contSupp k ⊆ S
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
⊢ TM2.SupportsStmt S (tr (Λ'.ret k))
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: S : Finset Λ'
q : Λ'
H₁ : Λ'.Supports S q
HS₁ : trStmts₁ q ⊆ S
⊢ Supports (trStmts₁ q) S

Tactic:
have W := fun {q} => trStmts₁_self q

Goal state after:
S : Finset Λ'
q : Λ'
H₁ : Λ'.Supports S q
HS₁ : trStmts₁ q ⊆ S
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
⊢ Supports (trStmts₁ q) S
Module: Mathlib.Topology.Category.LightProfinite.AsLimit

Goal state before:
pp: S : LightProfinite
n : ℕ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (S.transitionMap n))

Tactic:
apply Function.Surjective.of_comp (g := S.proj (n + 1))
  simpa only [proj_comp_transitionMap'] using S.proj_surjective n

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})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
h : (ConcreteCategory.hom (X.map (sigmaIncl f a).op)) x = (ConcreteCategory.hom (X.map (sigmaIncl f a).op)) y
⊢ (ConcreteCategory.hom (sigmaComparison X fun a ↦ ↑(fiber f a).toTop))
      ((ConcreteCategory.hom (X.mapIso (sigmaIso f).op).hom) x) a =
    (ConcreteCategory.hom (sigmaComparison X fun a ↦ ↑(fiber f a).toTop))
      ((ConcreteCategory.hom (X.mapIso (sigmaIso f).op).hom) y) a

Tactic:
← sigmaComparison_comp_sigmaIso

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})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
h :
  (ConcreteCategory.hom
        ((X.mapIso (sigmaIso f).op).hom ≫ (sigmaComparison X fun a ↦ ↑(fiber f a).toTop) ≫ ↾fun g ↦ g a))
      x =
    (ConcreteCategory.hom
        ((X.mapIso (sigmaIso f).op).hom ≫ (sigmaComparison X fun a ↦ ↑(fiber f a).toTop) ≫ ↾fun g ↦ g a))
      y
⊢ (ConcreteCategory.hom (sigmaComparison X fun a ↦ ↑(fiber f a).toTop))
      ((ConcreteCategory.hom (X.mapIso (sigmaIso f).op).hom) x) a =
    (ConcreteCategory.hom (sigmaComparison X fun a ↦ ↑(fiber f a).toTop))
      ((ConcreteCategory.hom (X.mapIso (sigmaIso f).op).hom) y) a
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: case e_a
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) ≫
      (functorIsoDiscreteAux₂ R Y✝).inv =
    (functorIsoDiscreteAux₂ R X✝).inv ≫
      (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f)

Tactic:
apply Sheaf.hom_ext

Goal state after:
case e_a
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ ((discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) ≫
        (functorIsoDiscreteAux₂ R Y✝).inv).hom =
    ((functorIsoDiscreteAux₂ R X✝).inv ≫
        (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)).map ((Functor.const CompHausᵒᵖ).map f)).hom
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: case e_a
P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ (discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) ≫
      (functorIsoDiscreteAux₂ R Y✝).inv =
    (functorIsoDiscreteAux₂ R X✝).inv ≫
      (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map ((Functor.const LightProfiniteᵒᵖ).map f)

Tactic:
apply Sheaf.hom_ext

Goal state after:
case e_a
P : TopCat → Prop
R : Type u
inst✝ : Ring R
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
⊢ ((discrete (ModuleCat R)).map ((underlying (ModuleCat R)).map ((functor R).map f)) ≫
        (functorIsoDiscreteAux₂ R Y✝).inv).hom =
    ((functorIsoDiscreteAux₂ R X✝).inv ≫
        (presheafToSheaf (coherentTopology LightProfinite) (ModuleCat R)).map
          ((Functor.const LightProfiniteᵒᵖ).map f)).hom
Module: Mathlib.Condensed.Light.Epi

Goal state before:
pp: n : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f✝ : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f✝ n)
X✝ Y✝ : Discrete ℕ ⥤ LightCondMod R
f : X✝ ⟶ Y✝
x✝ : Epi f
⊢ ∀ (j : Discrete ℕ),
    lim.map f ≫ limit.π Y✝ j =
      ((Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom) ≫ limit.π Y✝ j

Tactic:
intro ⟨n⟩

Goal state after:
n✝ : ℕ
R : Type u
inst✝¹ : Ring R
M N : ℕ → LightCondMod R
f✝ : (n : ℕ) → M n ⟶ N n
inst✝ : ∀ (n : ℕ), Epi (f✝ n)
X✝ Y✝ : Discrete ℕ ⥤ LightCondMod R
f : X✝ ⟶ Y✝
x✝ : Epi f
n : ℕ
⊢ lim.map f ≫ limit.π Y✝ { as := n } =
    ((Pi.isoLimit X✝).inv ≫ (Limits.Pi.map fun x ↦ f.app { as := x }) ≫ (Pi.isoLimit Y✝).hom) ≫ limit.π Y✝ { as := n }
Module: Mathlib.Condensed.Light.InternallyProjective

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

Tactic:
simp only [μIso_hom, μIso_inv, Functor.comp_map, δ_natural_right, assoc, δ_μ, comp_id]

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

Goal state before:
pp: α : Type u_1
xs : List α
⊢ List.traverse pure xs = pure xs

Tactic:
induction xs <;> simp! [*, List.traverse, functor_norm]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n✝¹ n✝ : ℕ
α✝ β✝ : TypeVec.{u} (n✝ + 1)
a : (α✝ ⊗ β✝) Fin2.fz
⊢ (id ⊗' id) Fin2.fz a = id Fin2.fz a

Tactic:
cases a; rfl

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : β ⟹ Subtype_ p
⊢ (toSubtype p ⊚ ofSubtype p) ⊚ f = f

Tactic:
toSubtype_of_subtype

Goal state after:
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : β ⟹ Subtype_ p
⊢ id ⊚ f = f
Module: Mathlib.Control.Traversable.Equiv

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

Tactic:
exact Equiv.lawfulFunctor eqv

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

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
⊢ Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))

Tactic:
rw [CompHausLike.mono_iff_injective]

Goal state after:
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
⊢ Function.Injective ⇑(ConcreteCategory.hom (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞})))
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
⊢ EffectiveEpi π'

Tactic:
rw [LightProfinite.effectiveEpi_iff_surjective, ← LightProfinite.epi_iff_surjective]

Goal state after:
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
this✝ : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
⊢ Epi π'
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: case cons
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
a✝ : l₁ ~ l₂
h : ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₂
this : cons <$> f x <*> ofList <$> Traversable.traverse f l₁ = cons <$> f x <*> ofList <$> Traversable.traverse f l₂
⊢ ofList <$> Traversable.traverse f (x :: l₁) = ofList <$> Traversable.traverse f (x :: l₂)

Tactic:
simpa [functor_norm] using! this

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ replace a b ⟦s⟧ = ⟦AList.replace a b s⟧

Tactic:
by
  simp [replace]

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, l₁.NodupKeys → l₂.NodupKeys → (l₁.kunion l₂).NodupKeys
l₂ : List (Sigma β)
nd₁ : (s :: l₁).NodupKeys
nd₂ : l₂.NodupKeys
⊢ ((s :: l₁).kunion l₂).NodupKeys

Tactic:
simp only [nodupKeys_cons] at nd₁

Goal state after:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, l₁.NodupKeys → l₂.NodupKeys → (l₁.kunion l₂).NodupKeys
l₂ : List (Sigma β)
nd₂ : l₂.NodupKeys
nd₁ : ¬s.fst ∈ l₁.keys ∧ l₁.NodupKeys
⊢ ((s :: l₁).kunion l₂).NodupKeys
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
p : l₁ ~ l₂
l : List (Sigma β)
⊢ l₁.kunion l ~ l₂.kunion l

Tactic:
by
  induction p generalizing l with
  | nil => rfl
  | cons hd _ ih =>
    simp [ih (List.kerase _ _)]
  | swap s₁ s₂ l => simp [kerase_comm, Perm.swap]
  | trans _ _ ih₁₂ ih₂₃ => exact Perm.trans (ih₁₂ l) (ih₂₃ l)

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
he : univ.sigma f = ∅
⊢ f = fun x ↦ ∅

Tactic:
simpa [funext_iff] using he

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.neLocus g = (f - g).support

Tactic:
by
  rw [← neLocus_add_right _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]

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

Goal state before:
pp: n m : ℕ
h : n < m
⊢ Ico n m = n :: Ico (n + 1) m

Tactic:
rw [← append_consecutive (Nat.le_succ n) h, succ_singleton]

Goal state after:
n m : ℕ
h : n < m
⊢ [n] ++ Ico n.succ m = n :: Ico (n + 1) m
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case cons.nil
α : Type u_1
f : α → α
l₁ : List α
hd : α
x✝ : [hd] ≠ []
⊢ modifyLast f (l₁ ++ [hd]) = l₁ ++ modifyLast f [hd]

Tactic:
simp only [modifyLast, modifyLast.go, Array.toListAppend_eq, nil_append]

Goal state after:
case cons.nil
α : Type u_1
f : α → α
l₁ : List α
hd : α
x✝ : [hd] ≠ []
⊢ modifyLast.go f (l₁ ++ [hd]) #[] = l₁ ++ [f hd]
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: α : Type u_1
f : α → α
l₁ l₂ : List α
x✝ : l₂ ≠ []
⊢ modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂

Tactic:
cases l₂ with
  | nil => contradiction
  | cons hd tl =>
    cases tl with
    | nil =>
      simp only [modifyLast, modifyLast.go, Array.toListAppend_eq, nil_append]
      exact modifyLast_concat _ hd _
    | cons hd' tl' =>
      rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
        modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
        modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
        append_assoc]
      all_goals { exact cons_ne_nil _ _ }

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β
p : l.Palindrome
⊢ (map f l).reverse = map f l

Tactic:
← map_reverse,

Goal state after:
α : Type u_1
β : Type u_2
l : List α
f : α → β
p : l.Palindrome
⊢ map f l.reverse = map f l
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
i : ℕ
hi : i < ((head :: tail).splitLengths l).length
⊢ ((head :: tail).splitLengths l)[i].length ≤ (head :: tail)[i]

Tactic:
simp only [splitLengths_cons]

Goal state after:
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih : ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length}, (tail.splitLengths l)[i].length ≤ tail[i]
l : List α
i : ℕ
hi : i < ((head :: tail).splitLengths l).length
⊢ (take head l :: tail.splitLengths (drop head l))[i].length ≤ (head :: tail)[i]
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : 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
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
mod_p : ∀ j < n + w.length, (take n w ++ w)[j]? = w[j % p]?
⊢ i % p < n + w.length

Tactic:
have : i % p < p := mod_lt i p_pos

Goal state after:
α : 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
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
mod_p : ∀ j < n + w.length, (take n w ++ w)[j]? = w[j % p]?
this : i % p < p
⊢ i % p < n + w.length
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
| ↑n.bitm1

Tactic:
rw [← zneg_zneg n]

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
| ↑(- -n).bitm1
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x : CofixA F n.succ
y : CofixA F (n.succ + 1)
i : F.B (head' x)
j : F.B (head' y)
h₀ : i ≍ j
h₁ : Agree x y
⊢ Agree (children' x i) (children' y j)

Tactic:
by
  obtain - | ⟨_, _, hagree⟩ := h₁; cases h₀
  apply hagree

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
X : Type w
f : X → ↑F X
i : X
n : ℕ
⊢ Agree (sCorec f i n) (sCorec f i n.succ)

Tactic:
induction n generalizing i with
  | zero => constructor
  | succ n n_ih => exact .intro _ _ fun _ => n_ih _

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (((match l with
            | nil => 0
            | node sz l x r => sz) +
            match m with
            | nil => 0
            | node sz l x r => sz) +
          1 +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      1 =
    (((match l with
          | nil => 0
          | node sz l x r => sz) +
          match m with
          | nil => 0
          | node sz l x r => sz) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      2

Tactic:
rw [add_right_comm _ 1]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h : (node size✝ l✝ x✝ r✝).Sized
h_mem : x ∈ node size✝ l✝ x✝ r✝
⊢ 0 < (node size✝ l✝ x✝ r✝).size

Tactic:
· { simp [h.1] }

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁

Tactic:
exact hr.dual.balanceL hl.dual (balance_sz_dual H)

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: p n : ℕ+
⊢ p ∈ n.factorMultiset.toPNatMultiset ↔ p.Prime ∧ p ∣ n

Tactic:
simp [factorMultiset, dvd_iff, PNat.Prime]

Goal state after:
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: case mp
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ p (PNat.find h) ∧ ∀ (n : ℕ+), n < PNat.find h → ¬p n

Tactic:
exact ⟨PNat.find_spec h, fun _ => PNat.find_min h⟩

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ls > rs
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ l',
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ r',
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ ∀ (a : α), All (fun y ↦ a < y) (Ordnode.node rs rl rx rr) → nil.Bounded (↑a) o₂

Tactic:
exact fun x h => hr.1.2.to_nil.mono_left (le_of_lt h.2.1)

Goal state after: