mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : t' α✝
⊢ traverse pure x✝ = pure 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✝ : t' α✝
⊢ Equiv.traverse eqv pure x✝ = pure x✝
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
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' α✝
⊢ traverse (Comp.mk ∘ map x✝² ∘ x✝¹) x✝ = Comp.mk (traverse x✝² <$> traverse 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
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 (Comp.mk ∘ map x✝² ∘ x✝¹) x✝ = Comp.mk (traverse x✝² <$> traverse x✝¹ x✝)
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' α✝
⊢ traverse (pure ∘ 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' α✝
⊢ Equiv.traverse eqv (pure ∘ x✝¹) x✝ = pure (x✝¹ <$> x✝)
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
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
x✝⁴ : ApplicativeTransformation F✝ G✝
x✝³ x✝² : Type u
x✝¹ : x✝³ → F✝ x✝²
x✝ : t' x✝³
⊢ (fun {α} ↦ x✝⁴.app α) (traverse x✝¹ x✝) = traverse ((fun {α} ↦ x✝⁴.app α) ∘ 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
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
x✝⁴ : ApplicativeTransformation F✝ G✝
x✝³ x✝² : Type u
x✝¹ : x✝³ → F✝ x✝²
x✝ : t' x✝³
⊢ (fun {α} ↦ x✝⁴.app α) (Equiv.traverse eqv x✝¹ x✝) = traverse ((fun {α} ↦ x✝⁴.app α) ∘ x✝¹) x✝
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q₂ : Semiquot α
s✝ : Set α
v₁ : Trunc ↑s✝
h : { s := s✝, val := v₁ }.s = q₂.s
⊢ { s := s✝, val := v₁ } = q₂

Tactic:
obtain ⟨_, v₂⟩ := q₂

Goal state after:
α : Type u_1
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ { s := s✝¹, val := v₁ } = { s := s✝, val := v₂ }
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_3
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ equiv ≍ Equiv.equivOfIsEmpty α (Fin 0)

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:
· refine heq_of_cast_eq ?_ (Subsingleton.allEq _ _)
      exact congrArg (α ≃ Fin ·) <| card_eq_zero

Goal state after:
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
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match f a with
    | some b => b :: l
    | none => lookmap.go f l (#[].push a)) =
    a :: lookmap.go f l #[]

Tactic:
rw [lookmap.go_append, lookmap, h]

Goal state after:
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match none with
    | some b => b :: l
    | none => (#[].push a).toListAppend (lookmap.go f l #[])) =
    a :: lookmap.go f l #[]
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case none
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ lookmap f (a :: l) =
    match none with
    | none => a :: lookmap f l
    | some b => b :: l

Tactic:
simp_all

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

Goal state before:
pp: case some
α : Type u_1
f : α → Option α
a : α
l : List α
val✝ : α
h : f a = some val✝
⊢ lookmap f (a :: l) =
    match some val✝ with
    | none => a :: lookmap f l
    | some b => b :: l

Tactic:
simp_all

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

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

Tactic:
by_cases h : k' = k
  · subst h; simp
  · simp_all [lookup_insert_ne h]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ extract a s = (lookup a s, erase a s)

Tactic:
simp [extract]; constructor <;> rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ s.max' hs < t.min' ht

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
ht : ¬t.Nonempty
p : α
hp : s.max' hs < p
⊢ (∀ x ∈ s, x < p) ∧ ∀ y ∈ t, p < y

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : t.Nonempty
p : α
hp : p < t.min' ht
⊢ (∀ x ∈ s, x < p) ∧ ∀ y ∈ t, p < y

Tactic:
simp_all

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ b ∈ lookupAll a (⟨a', b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ b ∈ lookupAll a (⟨a', b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Tactic:
· subst h
      simp [*, mem_lookupAll]

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ b ∈ lookupAll a (⟨a', b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : ¬t.Nonempty
p : α
⊢ (∀ x ∈ s, x < p) ∧ ∀ y ∈ t, p < y

Tactic:
simp_all

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

Goal state before:
pp: case trans
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b l₁✝ l₂✝ l₃✝ : List α'
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : ofList <$> Traversable.traverse f l₁✝ = ofList <$> Traversable.traverse f l₂✝
a_ih✝ : ofList <$> Traversable.traverse f l₂✝ = ofList <$> Traversable.traverse f l₃✝
⊢ ofList <$> Traversable.traverse f l₁✝ = ofList <$> Traversable.traverse f l₃✝

Tactic:
| trans =>

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : a = a'
h✝ : ¬decide (a = a') = true
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : ¬a = a'
h✝ : decide (a = a') = true
⊢ False

Tactic:
simp_all

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

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

Tactic:
if_true

Goal state after:
case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
⊢ ∅ = (image (const β✝) s).sup fun f ↦ ∅
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
a✝³ b✝ : Sigma β
a✝² : a✝³.fst ≠ b✝.fst
a✝¹ : decide (a = a✝³.fst) = true
a✝ : decide (a = b✝.fst) = true
⊢ False

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: case insert.refine_1.inr
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 ↦ f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), ↑j ≠ i
j : ι
hj✝ : j ∈ insert i s
hj : j ∈ s
⊢ (if hji : j = i then cast ⋯ a else g j ⋯) ∈ t j

Tactic:
· simpa [ne_of_mem_of_not_mem hj hi] using! hg _ _

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

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

Tactic:
simp [dedupKeys]

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✝ : α
⊢ f a✝ ≠ 0 a✝ ↔ f a✝ ≠ 0

Tactic:
Pi.zero_apply

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

Goal state before:
pp: case neg.h
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : DecidableEq κ
k✝ : κ
f : ι k✝ →₀ M
k : κ
i : ι k
h : ¬⟨k, i⟩.fst = k✝
⊢ ⟨k, i⟩ ∉ Set.range ⇑{ toFun := Sigma.mk k✝, inj' := ⋯ }

Tactic:
simp_all

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

Goal state before:
pp: n : ℕ
⊢ (bif !n.bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]

Tactic:
cases Nat.bodd n

Goal state after:
case false
n : ℕ
⊢ (bif !false then 1 else 0) + 2 * -[n+1].div2 = -[false.toNat + 2 * n.div2+1]

case true
n : ℕ
⊢ (bif !true then 1 else 0) + 2 * -[n+1].div2 = -[true.toNat + 2 * n.div2+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit m.succ = (↑n).testBit m

Tactic:
apply Nat.testBit_bit_succ

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

Goal state before:
pp: a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a ^ 2 = b ^ 2

Tactic:
by
  rw [sq, sq]
  exact natAbs_eq_iff_mul_self_eq

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

Goal state before:
pp: a b n : ℕ
a_le_n : a ≤ n
b_le_n : b ≤ n
⊢ |↑a - ↑b| ≤ ↑n

Tactic:
exact abs_sub_le_of_nonneg_of_le (natCast_nonneg a) (ofNat_le.mpr a_le_n)
    (natCast_nonneg b) (ofNat_le.mpr b_le_n)

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

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

Tactic:
← div_add_mod v r,

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.List.TakeWhile

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
l : List α
⊢ find? p [] = (dropWhile (fun x ↦ !p x) []).head?

pp: case cons
α : Type u_1
p : α → Bool
l : List α
head✝ : α
tail✝ : List α
tail_ih✝ : find? p tail✝ = (dropWhile (fun x ↦ !p x) tail✝).head?
⊢ find? p (head✝ :: tail✝) = (dropWhile (fun x ↦ !p x) (head✝ :: tail✝)).head?

Tactic:
case nil => simp

Goal state after:
case cons
α : Type u_1
p : α → Bool
l : List α
head✝ : α
tail✝ : List α
tail_ih✝ : find? p tail✝ = (dropWhile (fun x ↦ !p x) tail✝).head?
⊢ find? p (head✝ :: tail✝) = (dropWhile (fun x ↦ !p x) (head✝ :: tail✝)).head?
Module: Mathlib.Data.List.DropRight

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

Tactic:
rw [← length_reverse] at hk

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
⊢ map₂Right' f [] bs = (map (f none) bs, [])

Tactic:
cases bs <;> rfl

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

Goal state before:
pp: α : Type u
β : Type v
bs : List β
⊢ [].zipRight' bs = (map (fun b ↦ (none, b)) bs, [])

Tactic:
cases bs <;> rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
⊢ map₂Right f [] bs = map (f none) bs

Tactic:
cases bs <;> rfl

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

Goal state before:
pp: α : Type u
β : Type v
bs : List β
⊢ [].zipRight bs = map (fun b ↦ (none, b)) bs

Tactic:
cases bs <;> rfl

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

Goal state before:
pp: case inr.cons
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
head : α
tail : List α
⊢ Shortlex r s₁ (s₂ ++ head :: tail)

Tactic:
apply of_length_lt
    rw [List.length_append, List.length_cons]
    lia

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

Goal state before:
pp: case nil
α : Type u_1
l : List α
h : l.length ≤ [].sum
⊢ ([].splitLengths l).flatten = l

Tactic:
simp_all

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

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Bool
l : List α
this : (splitBy r l).flatten = l
x✝ : splitBy r l = []
⊢ l = []

Tactic:
simp_all

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

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Bool
l : List α
this : (splitBy r l).flatten = l
⊢ l = [] → splitBy r l = []

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
⊢ ¬[] ∈ splitBy.loop r l a g []

Tactic:
by
  induction l generalizing a g with
  | nil => simp [splitBy.loop]
  | cons b l IH =>
    rw [splitBy.loop]
    split
    · exact IH
    · rw [splitByLoop_eq_append, mem_append]
      simpa using IH

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

Goal state before:
pp: α : Type u_1
m : List α
r : α → α → Bool
l : List α
h : m ∈ splitBy r l
x✝ : m = []
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
lhs : ∀ i < w.length - p, w[i]? = w[i + p]?
drop : take p w ++ List.drop p w <+: take p w ++ w
⊢ w <+: take p w ++ w

Tactic:
simp_all

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 a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r [] a g gs)

Tactic:
rw [splitBy.loop, reverse_cons]

Goal state after:
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 a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (gs.reverse ++ [(a :: g).reverse])
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case inr.inl
α : Type u_1
p : ℕ
w : List α
per : w.HasPeriod p
p_pos : p > 0
dvd : p ∣ 0
len : 0 ≤ w.length
⊢ (take 0 w ++ w).HasPeriod p

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
this : ∀ i < n + w.length, (take n w ++ w)[i]? = (take n w ++ w)[i % p]?
⊢ ∀ i < (take n w ++ w).length, (take n w ++ w)[i]? = (take n w ++ w)[i % p]?

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : j < n
⊢ j < (take n w).length

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
j_mod : (j - n) % p = j % p
⊢ (take n w).length ≤ j

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_minus : j - n < w.length
n_le_j : n ≤ j
j_mod : (j - n) % p = j % p
⊢ w[j - (take n w).length]? = w[j - n]?

Tactic:
simp_all

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

Goal state before:
pp: case cons
α : Type u_1
m : List α
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {g : List α} {a : α},
    IsChain (fun x y ↦ r x y = true) (g.reverse ++ a :: l) →
      (∀ (x : α), x ∈ m.head? → r ((a :: l).getLast ⋯) x = false) →
        splitBy.loop r (l ++ m) a g [] = (g.reverse ++ a :: l) :: splitBy r m
g : List α
a : α
h : IsChain (fun x y ↦ r x y = true) (g.reverse ++ a :: b :: l)
ha : ∀ (x : α), x ∈ m.head? → r ((a :: b :: l).getLast ⋯) x = false
⊢ splitBy.loop r (b :: l ++ m) a g [] = (g.reverse ++ a :: b :: l) :: splitBy r m

Tactic:
simp_all [splitBy.loop]

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

Goal state before:
pp: case inr.inl
α : Type u_1
w : List α
p : ℕ
per_p : w.HasPeriod p
p_pos : p > 0
per_q : w.HasPeriod 0
len : p + 0 - p.gcd 0 ≤ w.length
⊢ w.HasPeriod (p.gcd 0)

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.gt
q_lt_p : q < p
gcd_lt_p : p.gcd q < p
per_diff : (drop q w).HasPeriod (p - q)
⊢ (take q w ++ drop q w ++ []).HasPeriod q

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
⊢ Function.Injective2 fromRows

Tactic:
by
  intro x1 x2 y1 y2
  simp [← Matrix.ext_iff]

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
x1 x2 : Matrix m n₁ R
y1 y2 : Matrix m n₂ R
⊢ (∀ (i : m) (j : n₁ ⊕ n₂), x1.fromCols y1 i j = x2.fromCols y2 i j) →
    (∀ (i : m) (j : n₁), x1 i j = x2 i j) ∧ ∀ (i : m) (j : n₂), y1 i j = y2 i j

Tactic:
simp_all

Goal state after:
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
y : α
hy : y ∈ Y ∧ ¬y < z
⊢ y ∈ Y

Tactic:
simp_all

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

Goal state before:
pp: case cons.mp
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h0 : a ≡ b [MOD m]
hs : ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
i : Fin (l.length + 1)
⊢ a ≡ b [MOD (m :: l).get i]

Tactic:
cases i using Fin.cases

Goal state after:
case cons.mp.zero
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h0 : a ≡ b [MOD m]
hs : ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
⊢ a ≡ b [MOD (m :: l).get 0]

case cons.mp.succ
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
h0 : a ≡ b [MOD m]
hs : ∀ (i : Fin l.length), a ≡ b [MOD l.get i]
i✝ : Fin l.length
⊢ a ≡ b [MOD (m :: l).get i✝.succ]