mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
⊢ (⟨a₂, b₂⟩ ∈ if a = ⟨a₁, b₂✝⟩.fst then some ⟨a, b⟩ else none) → ⟨a₁, b₂✝⟩.fst = ⟨a₂, b₂⟩.fst

Tactic:
dsimp

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
⊢ (⟨a₂, b₂⟩ ∈ if a = a₁ then some ⟨a, b⟩ else none) → a₁ = a₂
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
⊢ a ∈ (l₁.kunion l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys

Tactic:
by
  induction l₁ generalizing l₂ with
  | nil => simp
  | cons s l₁ ih => by_cases h : a = s.1 <;> [simp [h]; simp [h, ih]]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a)
hg : g = update f i ((f i).erase x)
hx' : x ∉ g i
⊢ f = update g i (insert x (g i))

Tactic:
rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
hr : r i x ((update g i (insert x (g i)) i).erase x)
hg : g = update f i ((f i).erase x)
hx' : x ∉ g i
⊢ f = update g i (insert x (g i))

Tactic:
rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x ((update g i (insert x (g i)) i).erase x)
hg : g = update f i ((f i).erase x)
hx' : x ∉ g i
⊢ f = update g i (insert x (g i))

Tactic:
rw [hg, update_idem, update_self, insert_erase x_mem, update_eq_self]

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

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ hd.support ∪ tl.sum.support = hd.support ⊔ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl

pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ _root_.Disjoint hd.support tl.sum.support

Tactic:
IH hl.right,

Goal state after:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ hd.support ∪ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl = hd.support ⊔ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl

case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ _root_.Disjoint hd.support tl.sum.support
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x (g i)
hx' : x ∉ g i
⊢ ∃ x_1 ∈ univ.sigma (update g i (insert x (g i))), x_1 ∉ univ.sigma g

pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
g : (a : ι) → Finset (α a)
ihs : ∀ t ⊂ univ.sigma (update g i (insert x (g i))), ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hr : r i x (g i)
hx' : x ∉ g i
⊢ ∀ (i_1 : ι), g i_1 ⊆ update g i (insert x (g i)) i_1

Tactic:
exacts [⟨⟨i, x⟩, mem_sigma.2 ⟨mem_univ _, by simp⟩, by simp [hx']⟩,
      (@le_update_iff _ _ _ _ g g i _).2 ⟨subset_insert _ _, fun _ _ ↦ le_rfl⟩]

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

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
i : ι k
m : M
⊢ (single i m).embSigma = single ⟨k, i⟩ m

Tactic:
by
  classical
  grind

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (i :: is) (d :: ds)

Tactic:
rw [← hiis]

Goal state after:
α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (↑t) (d :: ds)
Module: Mathlib.Data.Holor

Goal state before:
pp: case refine_2
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∀ (a : β) (s : Finset β),
    a ∉ s →
      ∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid →
        ∑ x ∈ insert a s, (f x).slice i hid = (∑ x ∈ insert a s, f x).slice i hid

Tactic:
· intro _ _ h_not_in ih
    rw [Finset.sum_insert h_not_in, ih, slice_add, Finset.sum_insert h_not_in]

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

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

case hn
m n i j : ℕ
⊢ -[i+1].bodd = (j.bodd ^^ (j + i + 1).bodd)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = (ofNat m).lor (ofNat n)

Tactic:
{rfl}

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

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]

Tactic:
{rfl}

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)

Tactic:
{rfl}

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]

Tactic:
{rfl}

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise and (ofNat m) (ofNat n) = (ofNat m).land (ofNat n)

Tactic:
{rfl}

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

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = (ofNat m).land -[n+1]

Tactic:
{rfl}

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

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)

Tactic:
{rfl}

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = -[m+1].land -[n+1]

Tactic:
{rfl}

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = -[m+1].land -[n+1]
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
{rfl}

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

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]

Tactic:
{rfl}

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) (ofNat m) -[n+1] = (ofNat m).ldiff -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)

Tactic:
{rfl}

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] (ofNat n) = -[m+1].ldiff (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]

Tactic:
{rfl}

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ bitwise (fun a b ↦ a && !b) -[m+1] -[n+1] = -[m+1].ldiff -[n+1]
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ 0 ^^^ b = b

Tactic:
zero_xor

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ b = b
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a = 0 ^^^ b ↔ a = b

Tactic:
zero_xor

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a = b ↔ a = b
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
m n : ℕ
⊢ bitwise xor (ofNat m) (ofNat n) = (ofNat m).xor (ofNat n)

Tactic:
{rfl}

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

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]

Tactic:
{rfl}

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ bitwise xor (ofNat m) -[n+1] = (ofNat m).xor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)

Tactic:
{rfl}

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ bitwise xor -[m+1] (ofNat n) = -[m+1].xor (ofNat n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = -[m+1].xor -[n+1]

Tactic:
{rfl}

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ bitwise xor -[m+1] -[n+1] = -[m+1].xor -[n+1]
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
⊢ (dropWhile p (head :: tail)).length ≤ (head :: tail).length

Tactic:
| cons head tail ih =>

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

Goal state before:
pp: case cons
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
⊢ mapIdxMAux' f arr.size (head :: tail) = mapIdxM.go f (head :: tail) arr *> pure PUnit.unit

Tactic:
| cons head tail ih =>

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

Goal state before:
pp: case neg
n m : ℕ
h : m ≤ n
⊢ IsChain (fun a b ↦ b = a.succ) (Ico n m)

Tactic:
rw [eq_nil_of_le h]
    exact .nil

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

Goal state before:
pp: n a b : ℕ
⊢ n < a ∨ b ≤ n ∨ n ∈ Ico a b

Tactic:
by
  grind [mem]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
⊢ (splitBy.loop r (b :: l) a g []).flatten = g.reverse ++ a :: b :: l

Tactic:
splitBy.loop,

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
⊢ (match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => splitBy.loop r l b [] [(a :: g).reverse]).flatten =
    g.reverse ++ a :: b :: l
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ splitBy.loop r [] a g []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
splitBy.loop,

Goal state after:
case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ [(a :: g).reverse].reverse
⊢ IsChain (fun x y ↦ r x y = true) m
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:
splitBy.loop,

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) ((a :: g).reverse :: gs).reverse
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
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 l a g gs)

Tactic:
induction l generalizing a g gs with
  | nil =>
    rw [splitBy.loop, reverse_cons]
    apply List.isChain_reverse.1
    simpa using isChain_cons.2 ⟨hga, hgs⟩
  | cons b l IH =>
    rw [splitBy.loop]
    split
    · refine IH hgs' hgs fun m hm ↦ ?_
      obtain ⟨ha, _, H⟩ := hga m hm
      refine ⟨ha, append_ne_nil_of_right_ne_nil _ (cons_ne_nil _ _), ?_⟩
      rwa [reverse_cons, head_append_of_ne_nil]
    · apply IH
      · simpa using hgs'
      · rw [reverse_cons]
        apply isChain_cons.2 ⟨hga, hgs⟩
      · simpa

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
h : ↑(n.choose (p ^ multiplicity p n)) ≡ 0 [ZMOD ↑p]
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
hm : n = p ^ multiplicity p n * m
⊢ False

Tactic:
nth_grw 1 [← mul_one (p ^ _), hm, choose_pow_mul_pow_mul_modEq_choose, choose_one_right] at h

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ False
Module: Mathlib.Data.Ordmap.Ordnode

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

pp: case nil.node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
size✝ : ℕ
l✝ : Ordnode α
lrx : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· exact node 2 l x nil

Goal state after:
case nil.node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
size✝ : ℕ
l✝ : Ordnode α
lrx : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

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

pp: case node.nil.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
size✝ : ℕ
l✝ : Ordnode α
lrx : α
r✝ : Ordnode α
⊢ Ordnode α

Tactic:
· exact node 2 l x nil

Goal state after:
case node.nil.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
size✝ : ℕ
l✝ : Ordnode α
lrx : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
| ↑n.bitm1 = ↑n + ↑n - 1

Tactic:
lhs
    rw [← zneg_zneg n]

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
| ↑(- -n).bitm1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
⊢ m ∣ n ↔ n % m = 0

Tactic:
rw [← dvd_to_int, Int.dvd_iff_emod_eq_zero, ← to_int_inj, mod_to_int]

Goal state after:
m n : ZNum
⊢ ↑n % ↑m = 0 ↔ ↑n % ↑m = ↑0
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ ⟨⟨a, f⟩.fst,
      splitFun (dropFun ⟨a, f⟩.snd)
        ((corec' P (fun b ↦ (g b).fst) (fun b ↦ dropFun (g b).snd) fun b ↦ lastFun (g b).snd) ∘ lastFun ⟨a, f⟩.snd)⟩ =
    (TypeVec.id ::: corec P g) <$$> ⟨a, f⟩

Tactic:
dsimp

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ ⟨a,
      splitFun (dropFun f)
        ((corec' P (fun b ↦ (g b).fst) (fun b ↦ dropFun (g b).snd) fun b ↦ lastFun (g b).snd) ∘ lastFun f)⟩ =
    (TypeVec.id ::: corec P g) <$$> ⟨a, f⟩
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ ¬r.dual.size + l.dual.size ≤ 1

pp: case refine_2
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ delta * r.dual.size < l.dual.size

pp: case refine_3
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ 2 * l.dual.size ≤ 9 * r.dual.size + 5 ∨ l.dual.size ≤ 3

Tactic:
· rwa [size_dual, size_dual, add_comm]

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ delta * r.dual.size < l.dual.size

case refine_3
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ 2 * l.dual.size ≤ 9 * r.dual.size + 5 ∨ l.dual.size ≤ 3
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.node4L x (node size✝ l✝ x✝ r✝) y r).size = l.size + (node size✝ l✝ x✝ r✝).size + r.size + 2

Tactic:
simp [node4L, node', size, hm.1]; abel

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hm : m.Sized
⊢ (l.node4L x m y r).size = l.size + m.size + r.size + 2

Tactic:
cases m
  · simp [node4L, node3L, node']
    abel
  · simp [node4L, node', size, hm.1]; abel

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

Goal state before:
pp: P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)
⊢ ∀ (x y : P.M), R x y → x = y

Tactic:
introv h'
  have := Inhabited.mk x.head
  apply eq_of_bisim R _ _ _ h'; clear h' x y
  constructor <;> introv ih <;> rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩ <;> clear h
  · replace h₀ := congr_arg Sigma.fst h₀
    replace h₁ := congr_arg Sigma.fst h₁
    simp only [dest_mk] at h₀ h₁
    rw [h₀, h₁]
  · simp only [dest_mk] at h₀ h₁
    cases h₀
    cases h₁
    apply h₂

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this✝ : MvFunctor.map g ∘ f = fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
this : f = fun i ↦ ⟨(f i).fst, (f i).snd⟩
⊢ (g <$$> P.wMk a f' fun i ↦ ⟨(f i).fst, (f i).snd⟩) =
    P.wMk a (g ⊚ f') fun i ↦ ⟨((fun i ↦ ⟨(f i).fst, (f i).snd⟩) i).fst, g ⊚ ((fun i ↦ ⟨(f i).fst, (f i).snd⟩) i).snd⟩

Tactic:
dsimp

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this✝ : MvFunctor.map g ∘ f = fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
this : f = fun i ↦ ⟨(f i).fst, (f i).snd⟩
⊢ (g <$$> P.wMk a f' fun i ↦ ⟨(f i).fst, (f i).snd⟩) = P.wMk a (g ⊚ f') fun i ↦ ⟨(f i).fst, g ⊚ (f i).snd⟩
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a.hm
m n : ℕ+
⊢ m.factorMultiset ≤ m.factorMultiset ⊔ n.factorMultiset

Tactic:
exact le_sup_left

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

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (nil.node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
this : (node lrs lrl lrx lrr).size ≤ 1
⊢ lrl.size = 0 ∧ lrr.size = 0

Tactic:
rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case refine_1.right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hba : b₁✝ ≤ b₂✝
hij : i < i
⊢ False

Tactic:
exact lt_irrefl _ hij

Goal state after: