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

Goal state before:
pp: case pred.refine_2
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
x✝ : q' = unrev q₂
x : Λ'
h' : x ∈ trStmts₁ (unrev q₂)
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂

pp: case pred.refine_3
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' ∈ trStmts₁ q₂
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂

Tactic:
· rcases Finset.mem_insert.1 h' with h' | h' <;> simp [h', unrev]

Goal state after:
case pred.refine_3
q' q₁ q₂ : Λ'
q₁_ih : q' ∈ trStmts₁ q₁ → trStmts₁ q' ⊆ trStmts₁ q₁
q₂_ih : q' ∈ trStmts₁ q₂ → trStmts₁ q' ⊆ trStmts₁ q₂
h : q' ∈ trStmts₁ q₂
x : Λ'
h' : x ∈ trStmts₁ q'
⊢ x = q₁.pred q₂ ∨ x = unrev q₂ ∨ x ∈ trStmts₁ q₁ ∨ x ∈ trStmts₁ q₂
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)
this✝ : (functor c).Initial
this : (StructuredArrow.toCostructuredArrow toLightProfinite c.pt).IsEquivalence
⊢ (functorOp c).Final

Tactic:
have : (functor c).rightOp.Final :=
    inferInstanceAs ((opOpEquivalence ℕ).inverse ⋙ (functor c).op).Final

Goal state after:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this✝¹ : (functor c).Initial
this✝ : (StructuredArrow.toCostructuredArrow toLightProfinite c.pt).IsEquivalence
this : (functor c).rightOp.Final
⊢ (functorOp c).Final
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
h :
  ∀ (a : Fiber ⇑f),
    (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) =
    (ConcreteCategory.hom (sigmaComparison X fun a ↦ ↑(fiber f a).toTop))
      ((ConcreteCategory.hom (X.mapIso (sigmaIso f).op).hom) y)

Tactic:
ext a

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
h :
  ∀ (a : Fiber ⇑f),
    (ConcreteCategory.hom (X.map (sigmaIncl f a).op)) x = (ConcreteCategory.hom (X.map (sigmaIncl f a).op)) y
a : Fiber ⇑f
⊢ (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.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 (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)

Tactic:
rw [show (Profinite.of PUnit.{u + 1}).const y ≫
    IsTerminal.from _ (fiber.{u, u + 1} f x) = 𝟙 _ from rfl]

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 (𝟙 (Profinite.of PUnit.{u + 1})).op)) (Function.Fiber.image (⇑f) x)
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case mp
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ ∃ u, q u

Tactic:
refine ⟨f <$$> u, ?_⟩

Goal state after:
case mp
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ q (f <$$> u)
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
F : f.Realizer
E : F.σ ≃ τ
x✝¹ : Set α
x✝ : x✝¹ ∈ F.F.toFilter.sets
t : F.σ
h : F.F.f t ⊆ x✝¹
⊢ (CFilter.ofEquiv E F.F).f (E t) ⊆ x✝¹

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
a : α
⊢ (mk a).out = a

Tactic:
by
  let h := (mk a).2; change Classical.choose h = a
  have := Classical.choose_spec h
  exact cast (congr_fun this a).symm rfl

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

Goal state before:
pp: n : ℕ
α : Type u_2
m : ℕ
h : m ≤ n
v : Fin n → α
⊢ (List.ofFn (take m h v)).length = (List.take m (List.ofFn v)).length

Tactic:
by simp [h]

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

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

Tactic:
by simp [h]

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

Goal state before:
pp: n : ℕ
α✝ : Fin n → Sort u_1
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
⊢ (List.take m (List.ofFn v)).length = m

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ e = { card := 1, equiv := Equiv.ofUnique α (Fin 1), decEq := fun a b ↦ decidableEq_of_subsingleton a b }

Tactic:
change FinEnum.mk e.1 e.2 = _
    congr 1
    · exact card_eq_one α
    · refine heq_of_cast_eq ?_ (Subsingleton.allEq _ _)
      exact congrArg (α ≃ Fin ·) <| card_eq_one α
    · subsingleton

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ e = { card := 1, equiv := Equiv.ofUnique α (Fin 1), decEq := fun a b ↦ decidableEq_of_subsingleton a b }

Tactic:
by
    change FinEnum.mk e.1 e.2 = _
    congr 1
    · exact card_eq_one α
    · refine heq_of_cast_eq ?_ (Subsingleton.allEq _ _)
      exact congrArg (α ≃ Fin ·) <| card_eq_one α
    · subsingleton

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
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 π')
this : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
⊢ (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π') ≫ snd S' ℕ∪{∞} =
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞} ≫ lift (𝟙 S') (CompHausLike.const S' ∞)) ≫
      snd S' ℕ∪{∞}

Tactic:
ext a

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 π')
this : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
a : ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
⊢ (ConcreteCategory.hom ((LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π') ≫ snd S' ℕ∪{∞})) a =
    (ConcreteCategory.hom
        ((LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞} ≫ lift (𝟙 S') (CompHausLike.const S' ∞)) ≫
          snd S' ℕ∪{∞}))
      a
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: α : Type u_1
x : Multiset α
⊢ traverse pure x = pure x

Tactic:
induction x using Quotient.inductionOn
  simp [traverse]

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

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
⊢ (if t = ∅ then ∅ else s) = (image (const β✝) s).sup fun f ↦ image f t

Tactic:
ext a

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
⊢ (a ∈ if t = ∅ then ∅ else s) ↔ a ∈ (image (const β✝) s).sup fun f ↦ image f t
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
⊢ (if s = ∅ then ∅ else t) = (image (const α✝ id) s).sup fun f ↦ image f t

Tactic:
ext a

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
⊢ (a ∈ if s = ∅ then ∅ else t) ↔ a ∈ (image (const α✝ id) s).sup fun f ↦ image f t
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
⊢ u <*> (t <*> s) = comp <$> u <*> t <*> s

Tactic:
ext a

Goal state after:
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ a ∈ u <*> (t <*> s) ↔ a ∈ comp <$> u <*> t <*> s
Module: Mathlib.Data.List.Sigma

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

Tactic:
by
  apply Perm.eraseP
  apply (nodupKeys_iff_pairwise.1 nd).imp
  intros; simp_all

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

Goal state before:
pp: α : 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:
by simp [h]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a ≠ a'
⊢ dlookup a (kinsert a' b' l) = dlookup a l

Tactic:
by simp [h]

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

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

Tactic:
induction xs with
  | nil => simp [dedupKeys]
  | cons x xs h =>
    simp only [dedupKeys_cons, kinsert_def, Sigma.eta]
    exact sizeOf_cons_le_sizeOf_cons x (le_trans (sizeOf_kerase x.fst xs.dedupKeys) h)

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
a' : α
snd✝ : β a'
h' : ¬a = a'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Tactic:
· simp [h', ih h]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ f.toAList.lookupFinsupp = f

Tactic:
ext a

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
⊢ f.toAList.lookupFinsupp a = f a
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case cons
ι : 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 : Pairwise (_root_.Disjoint on Finsupp.support) (hd :: tl)
⊢ (hd :: tl).sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ (hd :: tl)

Tactic:
simp only [List.pairwise_cons] at hl
    simp only [List.sum_cons, List.foldr_cons]
    rw [Finsupp.support_add_eq, IH hl.right, Finset.sup_eq_union]
    suffices _root_.Disjoint hd.support (tl.foldr (fun x y ↦ (Finsupp.support x ⊔ y)) ∅) by
      exact Finset.disjoint_of_subset_right (List.support_sum_subset _) this
    rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset,
      Finset.disjoint_sup_right]
    intro f hf
    simp only [List.mem_toFinset, List.mem_map] at hf
    obtain ⟨f, hf, rfl⟩ := hf
    exact hl.left _ hf

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

Goal state before:
pp: m n✝ k i n : ℕ
⊢ ↑m >>> (↑i + 1) = ↑(m <<< n >>> n >>> i >>> 1)

Tactic:
← Nat.shiftLeft_sub _ le_rfl,

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

Goal state before:
pp: m n✝ k i n : ℕ
⊢ ↑m >>> (↑i + 1) = ↑(m >>> i >>> 1)

Tactic:
← shiftRight_natCast,

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p (takeWhile p l) = takeWhile p l

Tactic:
takeWhile_takeWhile,

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile (fun a ↦ decide (p a = true ∧ p a = true)) l = takeWhile p l
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
h : Ico n m = []
⊢ m - n = 0

Tactic:
rw [← length, h, List.length]

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

Goal state before:
pp: n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n l

Tactic:
by
  rcases le_total n l with hnl | hln
  · rw [← append_consecutive hnl hlm, filter_append, filter_lt_of_top_le (le_refl l),
      filter_lt_of_le_bot (le_refl l), append_nil]
  · rw [eq_nil_of_le hln, filter_lt_of_le_bot hln]

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

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ (sz.splitLengths l)[i].length = sz[i]

Tactic:
have := map_splitLengths_length l sz h
  rw [← List.getElem_map List.length]
  · simp [this]
  · simpa using hi

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

Goal state before:
pp: α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
⊢ ∀ (l₂ : List α), l₂ ∈ sz.splitLengths l → l₂.length ≤ b

Tactic:
rw [List.forall_mem_iff_forall_getElem]
  intro i hi
  have := length_splitLengths_getElem_le l sz (hi := hi)
  have := h (sz[i]'(by simpa using hi)) (getElem_mem ..)
  lia

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]?
eq : j + u.length + p - u.length = j + p
⊢ (u ++ (v ++ w))[j + u.length + p]? = v[j + p]?

Tactic:
rw [getElem?_append_right]

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]?
eq : j + u.length + p - u.length = j + p
⊢ (v ++ w)[j + u.length + p - u.length]? = v[j + p]?

α : 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]?
eq : j + u.length + p - u.length = j + p
⊢ u.length ≤ j + u.length + p
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:
classical
  rintro ⟨X₁, Y₁, Z₁, -, rfl, rfl, hYZ₁⟩ ⟨X₂, Y₂, Z₂, hZ₂, hXZXY, rfl, hYZ₂⟩
  rw [add_comm X₁, add_comm X₂] at hXZXY
  refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
  · simpa [-not_and, not_and_or] using .inl hZ₂
  · rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]
  · rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]
    rwa [eq_comm]
  simp only [mem_add, or_imp, forall_and]
  refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
    by_cases z_in : z ∈ Y₂
    · obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
      exact ⟨w, .inl hw, hyz.trans hzw⟩
    · exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy
    exact ⟨z, .inl hz, hyz⟩

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

Goal state before:
pp: q₁ q₂ : ℚ≥0
⊢ q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

Tactic:
by
  convert! Rat.den_mul_den_eq_den_mul_gcd q₁ q₂
  norm_cast

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

Goal state before:
pp: n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n ↦ ↑n) (digits 10 n)
h : Even dig.length
this : (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum = -1 • dig.alternatingSum
⊢ dig.alternatingSum = 0

Tactic:
neg_one_zsmul

Goal state after:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun n ↦ ↑n) (digits 10 n)
h : Even dig.length
this : (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum = -dig.alternatingSum
⊢ dig.alternatingSum = 0
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case neg
p : ℕ → Prop
n : ℕ
hf : (Set.ofPred p).Finite
hn : #⋯.toFinset ≤ n
k : ℕ
hk : k ∈ {x | p x ∧ ∀ k < n, nth p k < x}
⊢ False

Tactic:
rcases exists_lt_card_nth_eq hk.1 with ⟨k, hlt, rfl⟩

Goal state after:
case neg
p : ℕ → Prop
n : ℕ
hf : (Set.ofPred p).Finite
hn : #⋯.toFinset ≤ n
k : ℕ
hlt : ∀ (hf : (Set.ofPred p).Finite), k < #hf.toFinset
hk : nth p k ∈ {x | p x ∧ ∀ k < n, nth p k < x}
⊢ False
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
⊢ f k < f n

Tactic:
apply hmono

Goal state after:
case x
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
⊢ k ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

case x
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
⊢ n ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

case a
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
k : ℕ
hk : k < n
⊢ k < n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
n : ZNum
⊢ ↑(ofZNum n) = ↑(↑n).toNat

Tactic:
by
  rw [← cast_to_nat, ofZNum_toNat]

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

Goal state before:
pp: a : ZNum
⊢ ↑(0 * a) = ↑0 * ↑a

Tactic:
by cases a <;> exact (zero_mul _).symm

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

Goal state before:
pp: m n : ZNum
h : Ordering.casesOn Ordering.gt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.gt = Ordering.lt

Tactic:
by simp [not_lt_of_gt h]

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

Goal state before:
pp: case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
⊢ (fun i ↦ (x.children i).approx n) = ch

Tactic:
ext a

Goal state after:
case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ (x.children a).approx n = ch a