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

Goal state before:
pp: case refine_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some (Λ'.clear (fun x ↦ decide (x = Γ'.consₗ)) main (unrev q)), var := o,
      stk := elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d }
    { l := some q, var := none, stk := elim (trNat L.headI ++ [Γ'.cons]) [] c d }

Tactic:
refine (clear_ok (splitAtPred_eq _ _ _ none [] ?_ ⟨rfl, rfl⟩)).trans ?_

Goal state after:
case refine_2.refine_1
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ ∀ x ∈ elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d main,
    decide (x = Γ'.consₗ) = false

case refine_2.refine_2
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ TransGen (fun a b ↦ b ∈ TM2.step tr a)
    { l := some (unrev q), var := none,
      stk := update (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [] }
    { l := some q, var := none, stk := elim (trNat L.headI ++ [Γ'.cons]) [] c d }
Module: Mathlib.Topology.Category.CompHausLike.SigmaComparison

Goal state before:
pp: P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
this :
  ∀ (x : ToType (X.obj (∏ᶜ fun a ↦ Opposite.op (of P (σ a))))),
    (ConcreteCategory.hom (Pi.π (fun b ↦ X.obj (Opposite.op (of P (σ b)))) a))
        ((ConcreteCategory.hom (piComparison X fun a ↦ Opposite.op (of P (σ a)))) x) =
      (ConcreteCategory.hom (X.map (Pi.π (fun a ↦ Opposite.op (of P (σ a))) a))) x
⊢ (ConcreteCategory.hom (sigmaComparison X σ)) x a =
    (ConcreteCategory.hom (Pi.π (fun a ↦ X.obj (Opposite.op (of P (σ a)))) a))
      ((ConcreteCategory.hom (piComparison X fun a ↦ Opposite.op (of P (σ a))))
        ((ConcreteCategory.hom
            (X.map
              (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a ↦ of P (σ a))
                  (productIsProduct fun x ↦ Opposite.op (of P (σ x)))).hom))
          x))

Tactic:
rw [this, ← comp_apply, ← Functor.map_comp]

Goal state after:
P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
this :
  ∀ (x : ToType (X.obj (∏ᶜ fun a ↦ Opposite.op (of P (σ a))))),
    (ConcreteCategory.hom (Pi.π (fun b ↦ X.obj (Opposite.op (of P (σ b)))) a))
        ((ConcreteCategory.hom (piComparison X fun a ↦ Opposite.op (of P (σ a)))) x) =
      (ConcreteCategory.hom (X.map (Pi.π (fun a ↦ Opposite.op (of P (σ a))) a))) x
⊢ (ConcreteCategory.hom (sigmaComparison X σ)) x a =
    (ConcreteCategory.hom
        (X.map
          ((opCoproductIsoProduct' (finiteCoproduct.isColimit fun a ↦ of P (σ a))
                (productIsProduct fun x ↦ Opposite.op (of P (σ x)))).hom ≫
            Pi.π (fun a ↦ Opposite.op (of P (σ a))) a)))
      x
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X✝ : Type w'
inst✝² : TopologicalSpace X✝
P : TopCat → Prop
X : TopCat
inst✝¹ : CompHausLike.HasExplicitFiniteCoproducts P
inst✝ : CompHausLike.HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
this : Preregular (CompHausLike P)
Z B : CompHausLike P
π : Z ⟶ B
he : EffectiveEpi π
⊢ IsQuotientMap ⇑(ConcreteCategory.hom ((CompHausLike.compHausLikeToTop P).map π))

Tactic:
exact .of_surjective_continuous (hs _ he) π.hom.hom.continuous

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

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

Tactic:
cases k with
  | halt => trivial
  | cons₁ => rw [contSupp_cons₁, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | cons₂ => rw [contSupp_cons₂, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
  | comp => rw [contSupp_comp] at H₁; exact fun _ => H₁ (codeSupp_self _ _ W)
  | fix =>
    rw [contSupp_fix] at H₁
    have L := @Finset.mem_union_left; have R := @Finset.mem_union_right
    intro s; dsimp only; cases natEnd (s.getD default)
    · refine H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)
    · exact H₁ (R _ <| L _ <| R _ <| R _ <| R _ <| Finset.mem_singleton_self _)

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

Goal state before:
pp: S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ Function.Surjective (⇑(ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(ConcreteCategory.hom (S.proj m)))

Tactic:
simpa only [proj_comp_transitionMapLE'] using S.proj_surjective n

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Cartesian

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop × ↑Y.toTop)
⊢ IsLimit (X.productCone Y)

Tactic:
by
  refine BinaryFan.isLimitMk (fun s ↦ ofHom _ { toFun x := (s.fst x, s.snd x) })
    (by rfl_cat) (by rfl_cat) fun _ _ h₁ h₂ ↦ ?_
  ext x
  exacts [ConcreteCategory.congr_hom h₁ _, ConcreteCategory.congr_hom h₂ _]

Goal state after:
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]
    intro s
    convert! (C_clopen s).2
    ext y
    simp [preimage_liftCover]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u} n
β : TypeVec.{v} n
f g : α ⟹ β
⊢ (∀ (i : Fin2 n), f i = g i) → f = g

Tactic:
intro h; funext i; apply h

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

Goal state before:
pp: case e_a
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
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
x✝² : β✝ → F✝ γ✝
x✝¹ : α✝ → G✝ β✝
x✝ : t' α✝
⊢ Equiv.traverse eqv x✝¹ x✝ = traverse x✝¹ x✝

Tactic:
rw [h₂]

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✝¹ : α✝ → β✝
x✝ : t' α✝
⊢ pure (Equiv.map eqv x✝¹ x✝) = pure (x✝¹ <$> x✝)

Tactic:
h₀

Goal state after:
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✝¹ : α✝ → β✝
x✝ : t' α✝
⊢ pure (Equiv.map eqv x✝¹ x✝) = pure (Equiv.map eqv x✝¹ x✝)
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ l.length - 1 ≤ 2 * count b l

Tactic:
by
  grind [hl.two_mul_count_bool_eq_ite]

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
b : Bool
⊢ 2 * count b l ≤ l.length + 1

Tactic:
by
  grind [hl.two_mul_count_bool_eq_ite]

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝¹ : FinEnum α
p : α → Prop
inst✝ : DecidablePred p
⊢ ∀ (x : { x // p x }), x ∈ List.filterMap (fun x ↦ if h : p x then some ⟨x, h⟩ else none) (toList α)

Tactic:
by rintro ⟨x, h⟩; simpa

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_4
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ (fun a b ↦ decEq a b) = fun a b ↦ decidableEq_of_subsingleton a b

Tactic:
· funext x
      exact ‹IsEmpty α›.elim x

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ ⟨a', b'⟩ :: kerase a' (⟨a, b⟩ :: kerase a s.entries) ~ ⟨a, b⟩ :: kerase a (⟨a', b'⟩ :: kerase a' s.entries)

Tactic:
rw [kerase_cons_ne, kerase_cons_ne, kerase_comm] <;>
    [apply Perm.swap; exact h; exact h.symm]

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

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

Tactic:
induction p with
  | nil => simp
  | cons a p IH =>
    cases h : f a
    · simpa [h] using IH (pairwise_cons.1 H).2
    · simp [lookmap_cons_some _ _ h, p]
  | swap a b l =>
    rcases h₁ : f a with - | c <;> rcases h₂ : f b with - | d
    · simpa [h₁, h₂] using Perm.swap _ _ _
    · simpa [h₁, lookmap_cons_some _ _ h₂] using Perm.swap _ _ _
    · simpa [lookmap_cons_some _ _ h₁, h₂] using Perm.swap _ _ _
    · rcases (pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) _ h₂ _ h₁ with ⟨rfl, rfl⟩
      exact Perm.refl _
  | trans p₁ _ IH₁ IH₂ =>
    refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))
    grind

Goal state after:
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:
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.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: tl = hd :: tl₁ ++ ⟨a, b⟩ :: tl₂

Tactic:
rw [h₂]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: (tl₁ ++ ⟨a, b⟩ :: tl₂) = hd :: tl₁ ++ ⟨a, b⟩ :: tl₂
Module: Mathlib.Data.List.Sigma

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

Tactic:
by_cases h : a = s.1 <;> [simp [h]; simp [h, ih]]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
⊢ Finset α

Tactic:
haveI := Classical.decEq α; haveI := Classical.decEq M
    exact (l.1.filter fun x => Sigma.snd x ≠ 0).keys.toFinset

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✝ : Zero N
f : α →₀ N
a✝ : α
⊢ a✝ ∈ f.neLocus 0 ↔ a✝ ∈ f.support

Tactic:
mem_neLocus,

Goal state after:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f : α →₀ N
a✝ : α
⊢ f a✝ ≠ 0 a✝ ↔ a✝ ∈ f.support
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ rdropWhile p (l ++ [x]) = rdropWhile p l

Tactic:
rw [rdropWhile_concat, if_pos h]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.reverse = l → l.Palindrome

Tactic:
refine bidirectionalRecOn l (fun _ => Palindrome.nil) (fun a _ => Palindrome.singleton a) ?_

Goal state after:
α : Type u_1
l : List α
⊢ ∀ (a : α) (l : List α) (b : α),
    (l.reverse = l → l.Palindrome) → (a :: (l ++ [b])).reverse = a :: (l ++ [b]) → (a :: (l ++ [b])).Palindrome
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = true
m : List α
hm : m ∈ gs.head?
ha : m ≠ []
w✝ : g.reverse ++ [a] ≠ []
H : r (m.getLast ha) ((g.reverse ++ [a]).head w✝) = false
⊢ r (m.getLast ha) (((a :: g).reverse ++ [b]).head ⋯) = false

Tactic:
rwa [reverse_cons, head_append_of_ne_nil]

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

Goal state before:
pp: case mp
α : Type u_1
m : List α
r : α → α → Bool
l : List (List α)
⊢ splitBy r m = l →
    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

Tactic:
rintro rfl
    exact ⟨(flatten_splitBy r m).symm, nil_notMem_splitBy r m, fun _ ↦ isChain_of_mem_splitBy,
      isChain_getLast_head_splitBy r m⟩

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))

Tactic:
← singleton_add,

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : {a} + M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (X - {a} + Y)

Tactic:
← singleton_add,

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = {a} + (X - {a} + Y)
Module: Mathlib.Data.Multiset.DershowitzManna

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

Tactic:
simp [hN, add_comm (_ + _)]

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

Goal state before:
pp: m n : ℕ
hm : m ≠ 1
⊢ m.Coprime n ! ↔ n < m.minFac

Tactic:
by
  rw [← not_le, iff_not_comm, Nat.Prime.not_coprime_iff_dvd]
  constructor
  · intro h
    exact ⟨m.minFac, minFac_prime hm, minFac_dvd m, Nat.dvd_factorial (minFac_pos m) h⟩
  · rintro ⟨p, hp, hdvd, hdvd'⟩
    exact le_trans (minFac_le_of_dvd hp.two_le hdvd) (hp.dvd_factorial.mp hdvd')

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

Goal state before:
pp: n : ℕ
p : (digits 10 n).Palindrome
h : Even (digits 10 n).length
⊢ 11 ∣ n

Tactic:
by
  let dig := (digits 10 n).map fun n : ℕ => (n : ℤ)
  replace h : Even dig.length := by rwa [List.length_map]
  refine eleven_dvd_iff.2 ⟨0, (?_ : dig.alternatingSum = 0)⟩
  have := dig.alternatingSum_reverse
  rw [(p.map _).reverse_eq, _root_.pow_succ', h.neg_one_pow, mul_one, neg_one_zsmul] at this
  exact eq_zero_of_neg_eq this.symm

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

Goal state before:
pp: 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

Tactic:
have : k ∣ n := by
      rw [← h, ← prod_factorization_pow_eq_self hn]
      apply prod_dvd_prod_of_subset_of_dvd <| support_mono hlt.le
      exact fun p _ ↦ Nat.pow_dvd_pow p <| hlt.le p

Goal state after:
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
this : k ∣ n
⊢ k ∈ ↑n.properDivisors
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: a : ℕ
l : List ℕ
hl : (a :: l).IsZeckendorfRep
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l

Tactic:
have hl' := hl

Goal state after:
a : ℕ
l : List ℕ
hl hl' : (a :: l).IsZeckendorfRep
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case refine_2
p : ℕ → Prop
x : ℕ
h : p x
hf : (Set.ofPred p).Infinite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
rw [← @Set.mem_ofPred_eq _ _ p, ← range_nth_of_infinite hf] at h

Goal state after:
case refine_2
p : ℕ → Prop
x : ℕ
h : x ∈ Set.range (nth p)
hf : (Set.ofPred p).Infinite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ count p (nth p n) = n

Tactic:
induction n with
  | zero => exact count_nth_zero _
  | succ k ihk =>
    rw [count_eq_card_filter_range, filter_range_nth_eq_insert hn, card_insert_of_notMem,
      ← count_eq_card_filter_range, ihk fun hf => lt_of_succ_lt (hn hf)]
    simp

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

Goal state before:
pp: case node
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l : l✝.Sized → C l✝
t_ih_r : r✝.Sized → C r✝
hl : (node size✝ l✝ x✝ r✝).Sized
⊢ C (node size✝ l✝ x✝ r✝)

Tactic:
rw [hl.eq_node']
    exact H1 _ _ _ (t_ih_l hl.2.1) (t_ih_r hl.2.2)

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

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x : F.M
⊢ Agree' n x x

Tactic:
induction n generalizing x with | zero => ?_ | succ _ n_ih => ?_ <;>
  induction x using PFunctor.M.casesOn'

Goal state after:
case zero.f
F : PFunctor.{uA, uB}
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ Agree' 0 (M.mk ⟨a✝, f✝⟩) (M.mk ⟨a✝, f✝⟩)

case succ.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ Agree' (n✝ + 1) (M.mk ⟨a✝, f✝⟩) (M.mk ⟨a✝, f✝⟩)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : Type u_1
inst✝ : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih✝ :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rl) o₂ →
      Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rr) o₂ →
      Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)) o₂
⊢ Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)).eraseMax ↑(findMax' x (Ordnode.node rs rl rx rr)) ∧
    (l.node' x (Ordnode.node rs rl rx rr)).size = (l.node' x (Ordnode.node rs rl rx rr)).eraseMax.size + 1

Tactic:
have := H.2.2.2.eq_node'

Goal state after:
case node
α : Type u_1
inst✝ : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih✝ :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rl) o₂ →
      Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rr) o₂ →
      Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
⊢ Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)).eraseMax ↑(findMax' x (Ordnode.node rs rl rx rr)) ∧
    (l.node' x (Ordnode.node rs rl rx rr)).size = (l.node' x (Ordnode.node rs rl rx rr)).eraseMax.size + 1