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

Goal state before:
pp: q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some (head main q), var := s, stk := elim (trList L) [] c d }
    { l := some q, var := none, stk := elim (trList [L.headI]) [] c d }

Tactic:
let o : Option Γ' := List.casesOn L none fun _ _ => some Γ'.cons

Goal state after:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn L none fun x x_1 ↦ some Γ'.cons
⊢ Reaches₁ (TM2.step tr) { l := some (head main q), var := s, stk := elim (trList L) [] c d }
    { l := some q, var := none, stk := elim (trList [L.headI]) [] c d }
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
⊢ IsTopologicalBasis {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V}

Tactic:
convert! IsTopologicalBasis.iInf_induced hT fun j (x : C.pt) => C.π.app j x using 1
  · exact induced_of_isLimit C hC
  ext U0
  constructor
  · rintro ⟨j, V, hV, rfl⟩
    let U : ∀ i, Set (F.obj i) := fun i => if h : i = j then by rw [h]; exact V else Set.univ
    refine ⟨U, {j}, ?_, ?_⟩
    · simp only [Finset.mem_singleton]
      rintro i rfl
      simpa [U]
    · simp [U]
  · rintro ⟨U, G, h1, h2⟩
    obtain ⟨j, hj⟩ := IsCofiltered.inf_objs_exists G
    let g : ∀ e ∈ G, j ⟶ e := fun _ he => (hj he).some
    let Vs : J → Set (F.obj j) := fun e => if h : e ∈ G then F.map (g e h) ⁻¹' U e else Set.univ
    let V : Set (F.obj j) := ⋂ (e : J) (_he : e ∈ G), Vs e
    refine ⟨j, V, ?_, ?_⟩
    · -- An intermediate claim used to apply induction along `G : Finset J` later on.
      have :
        ∀ (S : Set (Set (F.obj j))) (E : Finset J) (P : J → Set (F.obj j)) (_univ : Set.univ ∈ S)
          (_inter : ∀ A B : Set (F.obj j), A ∈ S → B ∈ S → A ∩ B ∈ S)
          (_cond : ∀ (e : J) (_he : e ∈ E), P e ∈ S), (⋂ (e) (_he : e ∈ E), P e) ∈ S := by
        intro S E
        induction E using Finset.induction_on with
        | empty =>
          intro P he _hh
          simpa
        | insert a E _ha hh1 =>
          intro hh2 hh3 hh4 hh5
          rw [Finset.set_biInter_insert]
          refine hh4 _ _ (hh5 _ (Finset.mem_insert_self _ _)) (hh1 _ hh3 hh4 ?_)
          intro e he
          exact hh5 e (Finset.mem_insert_of_mem he)
      -- use the intermediate claim to finish off the goal using `univ` and `inter`.
      refine this _ _ _ (univ _) (inter _) ?_
      intro e he
      dsimp [Vs]
      rw [dif_pos he]
      exact compat j e (g e he) (U e) (h1 e he)
    · -- conclude...
      rw [h2]
      change _ = (C.π.app j) ⁻¹' ⋂ (e : J) (_ : e ∈ G), Vs e
      rw [Set.preimage_iInter]
      apply congrArg
      ext1 e
      rw [Set.preimage_iInter]
      apply congrArg
      ext1 he
      simp [Vs, dif_pos he, ← Set.preimage_comp, ← coe_comp]

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

Goal state before:
pp: c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x ↦ Γ') Λ' (Option Γ')
⊢ x ∈ eval (TM2.step tr) i ↔ x ∈ halt <$> c.eval v

Tactic:
simp only [Part.map_eq_map, Part.mem_map_iff]

Goal state after:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step tr) (init c v) i
x : TM2.Cfg (fun x ↦ Γ') Λ' (Option Γ')
⊢ x ∈ eval (TM2.step tr) i ↔ ∃ a ∈ c.eval v, halt a = x
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.move p✝ k₁✝ k₂✝ q)
HS₁ : insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q) ⊆ S
h₁ : Λ'.move p✝ k₁✝ k₂✝ q ∈ S
h₂ : trStmts₁ q ⊆ S
h₃ : q ∈ S
⊢ Supports (insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q)) S

Tactic:
exact supports_insert.2 ⟨⟨fun _ => h₃, fun _ => h₁⟩, q_ih H₁ h₂⟩

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

Goal state before:
pp: case clear
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
p✝ : Γ' → Bool
k✝ : K'
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S (Λ'.clear p✝ k✝ q)
HS₁ : insert (Λ'.clear p✝ k✝ q) (trStmts₁ q) ⊆ S
h₁ : Λ'.clear p✝ k✝ q ∈ S
h₂ : trStmts₁ q ⊆ S
h₃ : q ∈ S
⊢ Supports (insert (Λ'.clear p✝ k✝ q) (trStmts₁ q)) S

Tactic:
exact supports_insert.2 ⟨⟨fun _ => h₃, fun _ => h₁⟩, q_ih H₁ h₂⟩

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

Goal state before:
pp: case fix.refine_1
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
k : Cont'
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h :
  codeSupp' f (Cont'.fix f k) ⊆ S ∧
    (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧ {Λ'.ret k} ⊆ S
H :
  (trStmts₁ (trNormal f.fix k) ⊆ S ∧
      codeSupp' f (Cont'.fix f k) ⊆ S ∧
        (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧
          {Λ'.ret k} ⊆ S) ∧
    contSupp k ⊆ S
⊢ codeSupp' f (Cont'.fix f k) ⊆ S ∧
    (trStmts₁ (trNormal f.fix k) ⊆ S ∧
        codeSupp' f (Cont'.fix f k) ⊆ S ∧
          (Λ'.clear natEnd main (trNormal f (Cont'.fix f k)) ∈ S ∧ trStmts₁ (trNormal f (Cont'.fix f k)) ⊆ S) ∧
            {Λ'.ret k} ⊆ S) ∧
      contSupp k ⊆ S

Tactic:
exact ⟨h.1, ⟨H.1.1, h⟩, H.2⟩

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

Goal state before:
pp: case refine_1.some.some
n m : ℕ
h : natUnionInftyEmbedding (Option.some n) = natUnionInftyEmbedding (Option.some m)
⊢ Option.some n = Option.some m

Tactic:
simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, inv_inj, add_left_inj,
        Nat.cast_inj] at h

Goal state after:
case refine_1.some.some
n m : ℕ
h : n = m
⊢ Option.some n = Option.some m
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:
rw [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
h_glue : ∀ (i j : S), ∀ x ∈ C i, x ∈ C j → i = j
s : S
y : Y
⊢ y ∈ liftCover C (fun i x ↦ i) h_glue C_cover_univ ⁻¹' {s} ↔ y ∈ C s

Tactic:
simp [preimage_liftCover]

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

Goal state before:
pp: case refine_3
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
⊢ liftCover C (fun i x ↦ i) h_glue C_cover_univ ∘ f = g

Tactic:
ext x
    simp [liftCover_of_mem <| Z_subset_C (g x) (by simpa [mem_image] using ⟨x, rfl, rfl⟩)]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : β → α → β
⊢ ∀ (x y : FreeMonoid α),
    op (↾flip (List.foldl f) (FreeMonoid.toList (x * y))) =
      op (↾flip (List.foldl f) (FreeMonoid.toList x)) * op (↾flip (List.foldl f) (FreeMonoid.toList y))

Tactic:
by
    intros
    simp only [FreeMonoid.toList_mul, List.foldl_append, Function.flip_def]
    rfl

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ ∀ (u : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }),
    (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y ↔
      (fun i t ↦ (↑t).1) <$$> f' rr n α <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> f' rr n α <$$> u = y

Tactic:
· intros
    simp +unfoldPartialApp only [map_map, TypeVec.comp]
    apply iff_of_eq -- Switch to `eq` so we can use `ext`
    congr <;> ext i ⟨x, _⟩ <;> cases i <;> rfl

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: w : ℕ
z : ℤ
⊢ { toFin := ↑z } = ↑z

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

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: w : ℕ
z : ℤ
⊢ (↑z).toFin = ↑z

Tactic:
by
  rw [← ofFin_intCast]

Goal state after:
Module: Mathlib.Data.BitVec

Goal state before:
pp: w n : ℕ
x : BitVec w
⊢ (↑n).toFin * x.toFin = n • x.toFin

Tactic:
open scoped Fin.CommRing in
    simp only [natCast_eq_ofNat, toFin_ofNat, Fin.ofNat_eq_cast, nsmul_eq_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : f.Realizer
x✝ : Set β
⊢ x✝ ∈ { f := fun s ↦ m '' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (map m f).sets

Tactic:
simp only [CFilter.toFilter, image_subset_iff, mem_ofPred_eq, Filter.mem_sets, mem_map]

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : f.Realizer
x✝ : Set β
⊢ (∃ b, F.F.f b ⊆ m ⁻¹' x✝) ↔ m ⁻¹' x✝ ∈ f
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case pos
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
hi : i = 0
⊢ ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
        ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e))
      i =
    e i

pp: case neg
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
hi : ¬i = 0
⊢ ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
        ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e))
      i =
    e i

Tactic:
· simp [hi]

Goal state after:
case neg
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
hi : ¬i = 0
⊢ ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => { toFun := fun i ↦ if i = 0 then a else b, inj' := ⋯ })
        ((fun e ↦ ⟨(e 0, e 1), ⋯⟩) e))
      i =
    e i
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
xs ys : AList β
⊢ Decidable (xs = ys)

Tactic:
AList.ext_iff

Goal state after:
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
xs ys : AList β
⊢ Decidable (xs.entries = ys.entries)
Module: Mathlib.Data.List.AList

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k k' : α
v : β k
h : ¬k' = k
⊢ lookup k' (insert k v l) = none ↔ k' ≠ k ∧ lookup k' l = none

Tactic:
simp_all [lookup_insert_ne h]

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

Goal state before:
pp: α : Type u
α' : Type u'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
β : Type v
l : List ((_ : α) × β)
f : α → α'
hf : Function.Injective f
a : α
⊢ dlookup (f a) (map (Sigma.map f fun x ↦ id) l) = dlookup a l

Tactic:
by
  have := dlookup_map (β' := fun _ => β) (f := f) (g := fun _ => id)
  grind [Option.map_id']

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

Goal state before:
pp: G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
eta : ApplicativeTransformation G H
α β : Type u_1
f : α → G β
x : Multiset α
⊢ (fun {α} ↦ eta.app α) (traverse f x) = traverse ((fun {α} ↦ eta.app α) ∘ f) x

Tactic:
by
  induction x using Quotient.inductionOn
  simp only [quot_mk_to_coe, traverse, lift_coe, Function.comp_apply,
    ApplicativeTransformation.preserves_map, LawfulTraversable.naturality]

Goal state after:
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
      simp_rw [seq_def, fmap_def]
      simp only [mem_sup, mem_image]
      constructor
      · rintro ⟨g, hg, b, ⟨f, hf, a, ha, rfl⟩, rfl⟩
        exact ⟨g ∘ f, ⟨comp g, ⟨g, hg, rfl⟩, f, hf, rfl⟩, a, ha, rfl⟩
      · rintro ⟨c, ⟨_, ⟨g, hg, rfl⟩, f, hf, rfl⟩, a, ha, rfl⟩
        exact ⟨g, hg, f a, ⟨f, hf, a, ha, rfl⟩, rfl⟩

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

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

Tactic:
change -[2 * Nat.div2 n+1] = _

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

Goal state before:
pp: m n : ℤ
⊢ bitwise (fun a b ↦ a && !b) m n = m.ldiff n

Tactic:
rcases m with m | m <;> rcases n with n | n <;> try {rfl}
    <;> simp only [bitwise, natBitwise, Bool.not_false,
      cond_false, cond_true, Nat.ldiff, Bool.and_true, negSucc.injEq,
      Bool.and_false, Bool.not_true, ldiff]

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ x && !!y) m n) = ↑(m &&& n)

case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x && !y)) m n = m ||| n

case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x && !!y) m n) = ↑(Nat.bitwise (fun a b ↦ a && !b) n m)
Module: Mathlib.Data.Int.CardIntervalMod

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

Tactic:
cast_add,

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

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

Tactic:
cast_add,

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
⊢ (drop k (l₂.reverse ++ l₁.reverse)).reverse = l₁ ++ l₂.rdrop k

Tactic:
drop_append_of_le_length hk,

Goal state after:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
⊢ (drop k l₂.reverse ++ l₁.reverse).reverse = l₁ ++ l₂.rdrop k
Module: Mathlib.Data.List.Intervals

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

Tactic:
by
  rcases le_total m l with hml | hlm
  · rw [min_eq_left hml, filter_lt_of_top_le hml]
  · rw [min_eq_right hlm, filter_lt_of_ge hlm]

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

Goal state before:
pp: case intro.intro.inr.cons
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h2len : (xa :: xs).length = (xa :: xb).length
h : Lex r xs xb
⊢ Acc (Shortlex r) (xa :: xs)

Tactic:
| @cons x xs _ h =>

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
i : ℕ
hi : i < (sz.splitLengths l).length
this : (sz.splitLengths l)[i].length ≤ sz[i]
⊢ (sz.splitLengths l)[i].length ≤ b

Tactic:
have := h (sz[i]'(by simpa using hi)) (getElem_mem ..)

Goal state after:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
this✝ : (sz.splitLengths l)[i].length ≤ sz[i]
this : sz[i] ≤ b
⊢ (sz.splitLengths l)[i].length ≤ b
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
p : ℕ
w : List α
⊢ w.HasPeriod p ↔ ∀ i < w.length, w[i]? = w[i % p]?

Tactic:
constructor
  · intro per i len
    exact Eq.symm (per.getElem?_mod p i w len)
  · intro mod
    rw [hasPeriod_iff_getElem?]
    intro i less
    rw [mod (i + p) (by lia), add_mod_right, mod i (by lia)]

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

Goal state before:
pp: case inr.inr.refine_2
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r l ++ splitBy r m)

Tactic:
isChain_append

Goal state after:
case inr.inr.refine_2
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r l) ∧
    IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r m) ∧
      ∀ (x : List α),
        x ∈ (splitBy r l).getLast? →
          ∀ (y : List α), y ∈ (splitBy r m).head? → ∃ ha hb, r (x.getLast ha) (y.head hb) = false
Module: Mathlib.Data.Nat.ChineseRemainder

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

Tactic:
have hlp : (l.map s).prod = (l'.map s).prod := List.Perm.prod_eq (List.Perm.map s hl)

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

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
n p : ℕ
h : p.Coprime n
m : ℕ
hm : ↑p ^ m = 0
this : ∃ a b, ↑p ^ m * a + ↑n * b = 1
⊢ IsUnit ↑n

Tactic:
obtain ⟨a, b, h⟩ := this

Goal state after:
A : Type u_1
inst✝ : CommRing A
n p : ℕ
h✝ : p.Coprime n
m : ℕ
hm : ↑p ^ m = 0
a b : A
h : ↑p ^ m * a + ↑n * b = 1
⊢ IsUnit ↑n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : nth p a = 0
⊢ nth p b = 0

Tactic:
simp only [nth_eq_zero, h₀, false_and, false_or] at ha ⊢

Goal state after:
p : ℕ → Prop
h₀ : ¬p 0
a b : ℕ
hab : a ≤ b
ha : ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ a
⊢ ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ b
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case succ.refine_1
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ {x | p x ∧ ∀ k < n + 1, nth p k < x}.Nonempty

Tactic:
use nth p (n + 1), nth_mem _ hn

Goal state after:
case right
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
⊢ ∀ k < n + 1, nth p k < nth p (n + 1)
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

Tactic:
· rcases id ll with _ | lls
      · rcases lr with _ | ⟨_, _, lrx⟩
        · exact node 2 l x nil
        · exact node 3 (ι lx) lrx ι x
      · rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)

Goal state after: