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

Goal state before:
pp: case pred
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : Λ'.Supports S q₁ → trStmts₁ q₁ ⊆ S → Supports (trStmts₁ q₁) S
q₂_ih : Λ'.Supports S q₂ → trStmts₁ q₂ ⊆ S → Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

Goal state after:
case pred
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : Λ'.Supports S q₁ → trStmts₁ q₁ ⊆ S → Supports (trStmts₁ q₁) S
q₂_ih : Λ'.Supports S q₂ → trStmts₁ q₂ ⊆ S → Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂) ⊆ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case ret
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : Cont'
H₁ : Λ'.Supports S (Λ'.ret k✝)
HS₁ : {Λ'.ret k✝} ⊆ S
⊢ Supports {Λ'.ret k✝} S

Tactic:
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁

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

Goal state before:
pp: case succ
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : unrev q ∈ S ∧ ∀ a ∈ trStmts₁ q, a ∈ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S

pp: case pred
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : Λ'.Supports S q₁ → trStmts₁ q₁ ⊆ S → Supports (trStmts₁ q₁) S
q₂_ih : Λ'.Supports S q₂ → trStmts₁ q₂ ⊆ S → Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S

pp: case ret
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : Cont'
H₁ : Λ'.Supports S (Λ'.ret k✝)
HS₁ : {Λ'.ret k✝} ⊆ S
⊢ Supports {Λ'.ret k✝} S

Tactic:
· refine supports_insert.2 ⟨⟨fun _ => h₁, fun _ => h₂.1, fun _ => h₂.1⟩, ?_⟩ -- succ
    exact supports_insert.2 ⟨⟨fun _ => h₂.2 _ W, fun _ => h₂.1⟩, q_ih H₁ h₂.2⟩

Goal state after:
case pred
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q₁ q₂ : Λ'
q₁_ih : Λ'.Supports S q₁ → trStmts₁ q₁ ⊆ S → Supports (trStmts₁ q₁) S
q₂_ih : Λ'.Supports S q₂ → trStmts₁ q₂ ⊆ S → Supports (trStmts₁ q₂) S
H₁ : Λ'.Supports S (q₁.pred q₂)
HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S
h₁ : q₁.pred q₂ ∈ S
h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S
⊢ Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S

case ret
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
k✝ : Cont'
H₁ : Λ'.Supports S (Λ'.ret k✝)
HS₁ : {Λ'.ret k✝} ⊆ S
⊢ Supports {Λ'.ret k✝} S
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})))
T : CompHausLike P
g : T ⟶ S
a : Fiber ⇑(comap (TopCat.Hom.hom g.hom) f)
x : ↑(fiber (comap (TopCat.Hom.hom g.hom) f) a).toTop
⊢ f ((ConcreteCategory.hom g) ↑x) = f ((ConcreteCategory.hom g) (preimage (⇑(comap (TopCat.Hom.hom g.hom) f)) a))

Tactic:
convert! map_eq_image _ _ x

Goal state after:
case e'_3
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})))
T : CompHausLike P
g : T ⟶ S
a : Fiber ⇑(comap (TopCat.Hom.hom g.hom) f)
x : ↑(fiber (comap (TopCat.Hom.hom g.hom) f) a).toTop
⊢ f ((ConcreteCategory.hom g) (preimage (⇑(comap (TopCat.Hom.hom g.hom) f)) a)) =
    Fiber.image (⇑(comap (TopCat.Hom.hom g.hom) f)) a
Module: Mathlib.Condensed.Epi

Goal state before:
pp: A : Type u'
inst✝⁸ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁷ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁶ : ConcreteCategory A FA
inst✝⁵ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁴ : (coherentTopology CompHaus).WEqualsLocallyBijective A
inst✝³ : HasSheafify (coherentTopology CompHaus) A
inst✝² : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)
inst✝¹ : Balanced (Sheaf (coherentTopology CompHaus) A)
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
⊢ Epi f ↔
    ∀ (S : CompHaus) (y : ToType (Y.obj.obj (op S))),
      ∃ S' φ, ∃ (_ : Function.Surjective ⇑(hom φ)), ∃ x, (hom (f.hom.app (op S'))) x = (hom (Y.obj.map (op φ))) y

Tactic:
by
  rw [← isLocallySurjective_iff_epi', coherentTopology.isLocallySurjective_iff,
    regularTopology.isLocallySurjective_iff]
  simp_rw [((CompHaus.effectiveEpi_tfae _).out 0 2 :)]

Goal state after:
Module: Mathlib.Data.Nat.Upto

Goal state before:
pp: p : ℕ → Prop
x : Upto p
h : ¬p ↑x
j : ℕ
h' : j < (↑x).succ
⊢ ¬p j

Tactic:
rcases Nat.lt_succ_iff_lt_or_eq.1 h' with (h' | rfl) <;> [exact x.2 _ h'; exact h]

Goal state after:
Module: Mathlib.Control.Fix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x✝ : α
hh : ¬(Fix.approx f (↑z) x).Dom
⊢ (assert (¬p ↑z) fun h ↦ hwf✝.fix (fixAux f) (z.succ h) x✝) = Fix.approx f (n + 1) x✝

Tactic:
succ_add_eq_add_succ

Goal state after:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + (↑z).succ)
hk : Nat.find h' = n + (↑z).succ
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x✝ : α
hh : ¬(Fix.approx f (↑z) x).Dom
⊢ (assert (¬p ↑z) fun h ↦ hwf✝.fix (fixAux f) (z.succ h) x✝) = Fix.approx f (n + 1) x✝
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
α : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x y : F α
⊢ ∀ (u : F fun i ↦ { p // (fun i x y ↦ ofRepeat (R i (prod.mk i x y))) i p.1 p.2 }),
    (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y ↔
      (prod.fst ⊚ subtypeVal R) <$$> toSubtype' R <$$> u = x ∧ (prod.snd ⊚ subtypeVal R) <$$> toSubtype' R <$$> u = y

Tactic:
by
    simp only [map_map, comp_assoc, subtypeVal_toSubtype']
    simp +unfoldPartialApp [comp]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij : i ≤ j
⊢ approx (⇑f) i ≤ approx (⇑f) j

Tactic:
induction j with

Goal state after:
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
α β γ : Type u
g : α → β
h : β → γ
x : t' α
⊢ Equiv.map eqv (h ∘ g) x = Equiv.map eqv h (Equiv.map eqv g x)

Tactic:
by
  simp [Equiv.map, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ s ∈ 𝓝 x

Tactic:
mem_nhds_toTopsp,

Goal state after:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
x : α
s : Set α
⊢ (∃ b, x ∈ F.f b ∧ F.f b ⊆ s) ↔ s ∈ 𝓝 x
Module: Mathlib.Data.ENat.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℕ∞
Hlt : ∀ i ∈ s, f i < g i
⊢ ∑ i ∈ s, f i < ∑ i ∈ s, g i

Tactic:
by
  induction hs using Nonempty.cons_induction with
  | singleton => simp [Hlt _ (mem_singleton_self _)]
  | cons _ _ _ _ ih =>
    simp only [sum_cons, forall_mem_cons] at Hlt ⊢
    exact ENat.add_lt_add Hlt.1 (ih Hlt.2)

Goal state after:
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
this : 0 ≤ ↑(2 * emax) - ↑prec
⊢ 0 ≤ ↑emax - (emin + ↑prec - 1)

Tactic:
simp only [emin, emax] at *

Goal state after:
C : FloatCfg
this : 0 ≤ ↑(2 * FloatCfg.emax) - ↑prec
⊢ 0 ≤ ↑FloatCfg.emax - (1 - ↑FloatCfg.emax + ↑prec - 1)
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
⊢ take 0 ⋯ v = fun i ↦ i.elim0

Tactic:
ext i; exact elim0 i

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
γ : Sort ?u.13
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ γ

Tactic:
refine
    (Quotient.liftOn s.entries
      (fun (l : List (Sigma β)) => (⟨_, fun nd => f ⟨l, nd⟩⟩ : Part γ))
      (fun l₁ l₂ p => Part.ext' (perm_nodupKeys p) ?_) : Part γ).get ?_
  · exact fun h1 h2 => H _ _ p
  · have := s.nodupKeys
    revert this
    rcases s.entries with ⟨l⟩
    exact id

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
snd_i : β a
⊢ ∃ x, x ≍ snd_i

Tactic:
simp only [exists_eq, heq_iff_eq]

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

Goal state before:
pp: case cons.inr
α : 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'
⊢ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) = dlookup a (⟨a', snd✝⟩ :: tail✝)

Tactic:
kunion_cons

Goal state after:
case cons.inr
α : 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'
⊢ dlookup a (⟨a', snd✝⟩ :: tail✝.kunion (kerase ⟨a', snd✝⟩.fst l₂)) = dlookup a (⟨a', snd✝⟩ :: tail✝)
Module: Mathlib.Data.Holor

Goal state before:
pp: ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun x1 x2 ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)
⊢ ↑(assocRight ⟨is, h⟩).drop.drop = ↑(drop ⟨is, h⟩)

Tactic:
simp [assocRight, drop, cast_type, List.drop_drop]

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

Goal state before:
pp: m n : ℕ
⊢ (subNatNat m n).bodd = (m.bodd ^^ n.bodd)

Tactic:
apply subNatNat_elim m n fun m n i => bodd i = xor m.bodd n.bodd <;>
  intro i j <;>
  simp only [Int.bodd, Nat.bodd_add]

Goal state after:
case hp
m n i j : ℕ
⊢ i.bodd = (j.bodd ^^ i.bodd ^^ j.bodd)

case hn
m n i j : ℕ
⊢ (!i.bodd) = (j.bodd ^^ (j.bodd ^^ i.bodd ^^ Nat.bodd 1))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: n : ℕ
⊢ (negOfNat n).bodd = n.bodd

Tactic:
cases n

Goal state after:
case zero
⊢ (negOfNat 0).bodd = Nat.bodd 0

case succ
n✝ : ℕ
⊢ (negOfNat (n✝ + 1)).bodd = (n✝ + 1).bodd
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: n : ℤ
⊢ (-n).bodd = n.bodd

Tactic:
cases n

Goal state after:
case ofNat
a✝ : ℕ
⊢ (-ofNat a✝).bodd = (ofNat a✝).bodd

case negSucc
a✝ : ℕ
⊢ (- -[a✝+1]).bodd = -[a✝+1].bodd
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat
f : Bool → Bool → Bool
n : ℤ
k a✝ : ℕ
⊢ (bitwise f (ofNat a✝) n).testBit k = f ((ofNat a✝).testBit k) (n.testBit k)

Tactic:
cases n

Goal state after:
case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f (ofNat a✝¹) (ofNat a✝)).testBit k = f ((ofNat a✝¹).testBit k) ((ofNat a✝).testBit k)

case ofNat.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f (ofNat a✝¹) -[a✝+1]).testBit k = f ((ofNat a✝¹).testBit k) (-[a✝+1].testBit k)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc
f : Bool → Bool → Bool
n : ℤ
k a✝ : ℕ
⊢ (bitwise f -[a✝+1] n).testBit k = f (-[a✝+1].testBit k) (n.testBit k)

Tactic:
cases n

Goal state after:
case negSucc.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f -[a✝¹+1] (ofNat a✝)).testBit k = f (-[a✝¹+1].testBit k) ((ofNat a✝).testBit k)

case negSucc.negSucc
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (bitwise f -[a✝¹+1] -[a✝+1]).testBit k = f (-[a✝¹+1].testBit k) (-[a✝+1].testBit k)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℕ
⊢ ↑m >>> ↑n = ↑(m >>> n)

Tactic:
cases n

Goal state after:
case zero
m : ℕ
⊢ ↑m >>> ↑0 = ↑(m >>> 0)

case succ
m n✝ : ℕ
⊢ ↑m >>> ↑(n✝ + 1) = ↑(m >>> (n✝ + 1))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℕ
⊢ -[m+1] >>> ↑n = -[m >>> n+1]

Tactic:
cases n

Goal state after:
case zero
m : ℕ
⊢ -[m+1] >>> ↑0 = -[m >>> 0+1]

case succ
m n✝ : ℕ
⊢ -[m+1] >>> ↑(n✝ + 1) = -[m >>> (n✝ + 1)+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n✝ k i n : ℕ
⊢ Nat.shiftLeft' true m i = Nat.shiftLeft' true m (n + i - n)

pp: case a
m n✝ k i n : ℕ
⊢ n ≤ n + i

Tactic:
Nat.add_sub_cancel_left

Goal state after:
m n✝ k i n : ℕ
⊢ Nat.shiftLeft' true m i = Nat.shiftLeft' true m i

case a
m n✝ k i n : ℕ
⊢ n ≤ n + i
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: case append_singleton
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n : ℕ
⊢ take ((xs ++ [x]).length - n) (xs ++ [x]) = (drop n (xs ++ [x]).reverse).reverse

Tactic:
cases n

Goal state after:
case append_singleton.zero
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
⊢ take ((xs ++ [x]).length - 0) (xs ++ [x]) = (drop 0 (xs ++ [x]).reverse).reverse

case append_singleton.succ
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), take (xs.length - n) xs = (drop n xs.reverse).reverse
n✝ : ℕ
⊢ take ((xs ++ [x]).length - (n✝ + 1)) (xs ++ [x]) = (drop (n✝ + 1) (xs ++ [x]).reverse).reverse
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: case append_singleton
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n : ℕ
⊢ drop ((xs ++ [x]).length - n) (xs ++ [x]) = (take n (xs ++ [x]).reverse).reverse

Tactic:
cases n

Goal state after:
case append_singleton.zero
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
⊢ drop ((xs ++ [x]).length - 0) (xs ++ [x]) = (take 0 (xs ++ [x]).reverse).reverse

case append_singleton.succ
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n✝ : ℕ
⊢ drop ((xs ++ [x]).length - (n✝ + 1)) (xs ++ [x]) = (take (n✝ + 1) (xs ++ [x]).reverse).reverse
Module: Mathlib.Data.List.DropRight

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

Tactic:
by
  rw [← rdrop_add, rdrop_append_length]

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

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

Tactic:
filter_append,

Goal state after:
case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ filter (fun x ↦ decide (x < l)) (Ico n l) ++ filter (fun x ↦ decide (x < l)) (Ico l m) = Ico n l
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
n : ℕ
hn : n ≤ tl.length + 1
m : ℕ
hm : m ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) n = (fun k ↦ (hd :: tl).insertIdx k x) m
hx : ¬x = hd ∧ ¬x ∈ tl
⊢ n = m

Tactic:
cases n

Goal state after:
case cons.zero
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
m : ℕ
hm : m ≤ tl.length + 1
hx : ¬x = hd ∧ ¬x ∈ tl
hn : 0 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) 0 = (fun k ↦ (hd :: tl).insertIdx k x) m
⊢ 0 = m

case cons.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
m : ℕ
hm : m ≤ tl.length + 1
hx : ¬x = hd ∧ ¬x ∈ tl
n✝ : ℕ
hn : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) m
⊢ n✝ + 1 = m
Module: Mathlib.Data.List.Intervals

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

Tactic:
filter_append,

Goal state after:
case inl
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n l) ++ filter (fun x ↦ decide (l ≤ x)) (Ico l m) = Ico l m
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x ∈ hd :: tl
n : ℕ
hn : n ∈ {n | n ≤ (hd :: tl).length}
m : ℕ
hm : m ∈ {n | n ≤ (hd :: tl).length}
h : (fun k ↦ (hd :: tl).insertIdx k x) n = (fun k ↦ (hd :: tl).insertIdx k x) m
⊢ n = m

Tactic:
simp only [length, Set.mem_ofPred_eq] at hn hm
    simp only [mem_cons, not_or] at hx
    cases n <;> cases m
    · rfl
    · simp [hx.left] at h
    · simp [Ne.symm hx.left] at h
    · simp only [insertIdx_succ_cons, cons.injEq, true_and] at h
      rw [Nat.succ_inj]
      refine IH hx.right ?_ ?_ h
      · simpa [Nat.succ_le_succ_iff] using hn
      · simpa [Nat.succ_le_succ_iff] using hm

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
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
⊢ IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (gs.reverse ++ [(a :: g).reverse]).reverse

Tactic:
simpa using isChain_cons.2 ⟨hga, hgs⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Semiring R
inst✝² : NonUnitalSemiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m n A
b : Matrix n o A
⊢ mulRightLinearMap l R (a * b) = mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a

Tactic:
by
  ext
  simp only [mulRightLinearMap_apply, LinearMap.comp_apply, Matrix.mul_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.DualNumber

Goal state before:
pp: case h2
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ ∑ x, (fst (A i✝ x) * snd (B x j✝) + snd (A i✝ x) * fst (B x j✝)) =
    ∑ x, fst (A i✝ x) * snd (B x j✝) + ∑ x, snd (A i✝ x) * fst (B x j✝)

Tactic:
← Finset.sum_add_distrib

Goal state after:
case h2
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
i✝ j✝ : n
⊢ ∑ x, (fst (A i✝ x) * snd (B x j✝) + snd (A i✝ x) * fst (B x j✝)) =
    ∑ x, (fst (A i✝ x) * snd (B x j✝) + snd (A i✝ x) * fst (B x j✝))
Module: Mathlib.Data.Multiset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ ∏ x ∈ s.toFinset, (count x s + 1 - count x 0) = ∏ i ∈ s.toFinset, (count i s + 1)

Tactic:
count_zero,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ ∏ x ∈ s.toFinset, (count x s + 1 - 0) = ∏ i ∈ s.toFinset, (count i s + 1)
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case cons.inr.refine_1
α : 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
⊢ M = X + Y' + (Y - Y')

Tactic:
add_add_tsub_cancel (filter_le ..),

Goal state after:
case cons.inr.refine_1
α : 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
⊢ M = X + Y
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: a : ℚ≥0
b : ℕ
⊢ (fun q ↦ ⌈↑q⌉₊) a ≤ b ↔ ↑a ≤ ↑↑b

Tactic:
Nat.ceil_le

Goal state after:
a : ℚ≥0
b : ℕ
⊢ ↑a ≤ ↑b ↔ ↑a ≤ ↑↑b
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: a : ℚ≥0
b : ℕ
⊢ (fun q ↦ ⌈↑q⌉₊) a ≤ b ↔ a ≤ ↑b

Tactic:
by rw [← NNRat.coe_le_coe, Nat.ceil_le]; norm_cast

Goal state after:
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case property
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k // ∀ i ∈ l, k ≡ a i [MOD s i] }
k : { k // k ≡ a i [MOD s i] ∧ k ≡ ↑ih [MOD (List.map s l).prod] }
⊢ ∀ i_1 ∈ i :: l, ↑k ≡ a i_1 [MOD s i_1]

Tactic:
simp only [List.mem_cons, forall_eq_or_imp, k.prop.1, true_and]

Goal state after:
case property
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k // ∀ i ∈ l, k ≡ a i [MOD s i] }
k : { k // k ≡ a i [MOD s i] ∧ k ≡ ↑ih [MOD (List.map s l).prod] }
⊢ ∀ a_1 ∈ l, ↑k ≡ a a_1 [MOD s a_1]
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
p : ℕ
hp₁ : Nat.Prime p
hp₂ : p ∣ (Icc 1 (n - 1)).gcd n.choose
hp₃ : ¬(Icc 1 (n - 1)).gcd n.choose = 0
this : Fact (Nat.Prime p)
⊢ p = n.minFac

Tactic:
simp_rw [Finset.dvd_gcd_iff, ← modEq_zero_iff_dvd] at hp₂

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
p : ℕ
hp₁ : Nat.Prime p
hp₃ : ¬(Icc 1 (n - 1)).gcd n.choose = 0
this : Fact (Nat.Prime p)
hp₂ : ∀ b ∈ Icc 1 (n - 1), n.choose b ≡ 0 [MOD p]
⊢ p = n.minFac
Module: Mathlib.Data.Nat.Nth

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

Tactic:
← range_nth_of_infinite hf

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.Num.Prime

Goal state before:
pp: case neg
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ (↑n).sqrt < fuel + ↑k.succ.bit1

Tactic:
convert! Nat.lt_succ_of_lt h using 1

Goal state after:
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ fuel + ↑k.succ.bit1 = (fuel + 1 + ↑k.bit1).succ