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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
⊢ (map f (x :: xs)).dedup = map f (x :: xs).dedup

Tactic:
map_cons

Goal state after:
case cons
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
⊢ f x :: map f xs.dedup = map f (x :: xs.dedup)

Tactic:
map_cons

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
⊢ f x :: map f xs.dedup = f x :: map f xs.dedup
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : head✝ ∈ l₂
⊢ head✝ ∈ l₂

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := ⋯
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ xs ~ ys

Tactic:
assumption

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

Goal state before:
pp: case empty
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ 0 ∩ t ≤ t

Tactic:
exact (zero_inter t).symm ▸ zero_le _

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ u + s = u ∪ s ∧ s = t

pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ s ∧ s = t → u + s = u ∪ t

Tactic:
· rw [and_iff_right_of_imp]
    · exact (Multiset.le_of_add_le_add_left <| h0.trans_le <| union_le_add u t).antisymm h
    · rintro rfl
      exact h0

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ s ∧ s = t → u + s = u ∪ t
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
xs : List α
x head✝ : α
⊢ [head✝] <:+: [x] ↔ [head✝] = [] ∨ [head✝] = [x]

Tactic:
simp [List.singleton_infix_singleton_iff]

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

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ (a :: l).tails = (map reverse (a :: l).reverse.inits).reverse

Tactic:
simp [tails_eq_inits l]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (insert a t) s ↔ a ∉ s ∧ Disjoint s t

Tactic:
rw [disjoint_insert_left, _root_.disjoint_comm]

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

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ (range n).Nontrivial

Tactic:
by
  rw [Finset.Nontrivial, Finset.coe_range]
  exact ⟨0, by grind, 1, hn, Nat.zero_ne_one⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
x✝ : ↥(map f s)
x : β
hx : x ∈ map f s
⊢ ∃ a, (fun x ↦ ⟨f ↑x, ⋯⟩) a = ⟨x, hx⟩

Tactic:
obtain ⟨x, hxs, rfl⟩ := mem_map.mp hx

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
x✝ : ↥(map f s)
x : α
hxs : x ∈ s
hx : f x ∈ map f s
⊢ ∃ a, (fun x ↦ ⟨f ↑x, ⋯⟩) a = ⟨f x, hx⟩
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i.rev.rev = j.rev ↔ i = j.rev

Tactic:
rev_rev

Goal state after:
n : ℕ
i j : Fin n
⊢ i = j.rev ↔ i = j.rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ j.rev < i.rev.rev ↔ j.rev < i

Tactic:
rev_rev

Goal state after:
n : ℕ
i j : Fin n
⊢ j.rev < i ↔ j.rev < i
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ j.rev ≤ i.rev.rev ↔ j.rev ≤ i

Tactic:
rev_rev

Goal state after:
n : ℕ
i j : Fin n
⊢ j.rev ≤ i ↔ j.rev ≤ i
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ j.rev.rev < i.rev ↔ j < i.rev

Tactic:
rev_rev

Goal state after:
n : ℕ
i j : Fin n
⊢ j < i.rev ↔ j < i.rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ j.rev.rev ≤ i.rev ↔ j ≤ i.rev

Tactic:
rev_rev

Goal state after:
n : ℕ
i j : Fin n
⊢ j ≤ i.rev ↔ j ≤ i.rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h : i ≠ 0
h' : i.rev ≠ last n
⊢ (i.pred h).rev = i.rev.castPred h'

Tactic:
by
  rw [← castSucc_inj, castSucc_castPred, ← rev_succ, succ_pred]

Goal state after:
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ i.castSucc = i.rev.rev.castSucc

Tactic:
rev_rev

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ i.castSucc = i.castSucc
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
⊢ i.succ = i.rev.rev.succ

Tactic:
rev_rev

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
⊢ i.succ = i.succ
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i.rev = (p.succAbove i.rev).rev.rev

Tactic:
rev_rev

Goal state after:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i.rev = p.succAbove i.rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ (p.succAbove i).rev = (p.succAbove i.rev.rev).rev

Tactic:
rev_rev

Goal state after:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ (p.succAbove i).rev = (p.succAbove i).rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ i = i.rev.rev

Tactic:
rev_rev

Goal state after:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ i = i
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ i = i.rev.rev

Tactic:
rev_rev

Goal state after:
case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ i = i
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ p.predAbove i.rev = (p.predAbove i.rev).rev.rev

Tactic:
rev_rev

Goal state after:
n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ p.predAbove i.rev = p.predAbove i.rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ (p.predAbove i).rev = (p.predAbove i.rev.rev).rev

Tactic:
rev_rev

Goal state after:
n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ (p.predAbove i).rev = (p.predAbove i).rev
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ #(Finset.subtype p s) = #(filter p s)

Tactic:
simp [Finset.subtype]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ i.castPred hi < j ↔ i < j.castSucc

Tactic:
← castSucc_lt_castSucc_iff,

Goal state after:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ (i.castPred hi).castSucc < j.castSucc ↔ i < j.castSucc
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ j < i.castPred hi ↔ j.castSucc < i

Tactic:
← castSucc_lt_castSucc_iff,

Goal state after:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ j.castSucc < (i.castPred hi).castSucc ↔ j.castSucc < i
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
⊢ ↑(image f s) = ↑t

Tactic:
by simp [hsurj.image_eq_of_mapsTo hf]

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

Goal state before:
pp: α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ (ofFn fun i ↦ ofFn fun j ↦ Fin.repeat n a ⟨↑i * m + ↑j, ⋯⟩).flatten = (replicate n (ofFn a)).flatten

Tactic:
← ofFn_const,

Goal state after:
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ (ofFn fun i ↦ ofFn fun j ↦ Fin.repeat n a ⟨↑i * m + ↑j, ⋯⟩).flatten = (ofFn fun x ↦ ofFn a).flatten
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
hi : i ≠ last (n + 1)
⊢ (last n).predAbove i = i.castPred hi

Tactic:
by
  rw [← exists_castSucc_eq] at hi
  rcases hi with ⟨y, rfl⟩
  exact predAbove_last_castSucc

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
⊢ append xs ys i.rev.rev = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i.rev)

Tactic:
rev_rev

Goal state after:
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
⊢ append xs ys i = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i.rev)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
i : Fin (m + n)
⊢ addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) i = v i

Tactic:
cases i using addCases <;> simp

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

Goal state before:
pp: case neg.cons
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
a✝ : [x, x] <+ l
⊢ [x, x] <+ l

Tactic:
assumption

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case cast
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin n
⊢ snoc (update p i y) x j.castSucc = update (snoc p x) i.castSucc y j.castSucc

Tactic:
rcases eq_or_ne j i with rfl | hne <;> simp [*]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case cast
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin n
⊢ snoc (update p i y) x j.castSucc = update (snoc p x) i.castSucc y j.castSucc

Tactic:
| cast j =>

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case succ.cast
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
j : Fin n
⊢ cons a (snoc q b) j.castSucc.succ = snoc (cons a q) b j.castSucc.succ

Tactic:
| cast j =>

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case cast.cast
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i j : Fin n
h : snoc x x₀ i.castSucc = snoc x x₀ j.castSucc
⊢ i.castSucc = j.castSucc

Tactic:
| cast j =>

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case last.cast
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin n
h : snoc x x₀ (last n) = snoc x x₀ j.castSucc
⊢ last n = j.castSucc

Tactic:
| cast j =>

Goal state after:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Sort u_4
β : Sort u_5
inst✝ : Finite β
f : α → β
H : Injective f
n : ℕ
e : β ≃ Fin n
⊢ Finite α

Tactic:
classical exact .of_equiv (Set.range (e ∘ f)) (Equiv.ofInjective _ (e.injective.comp H)).symm

Goal state after:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b : α
⊢ a = b

Tactic:
let ⟨x, hx⟩ := card_eq_one_iff.1 ha.symm

Goal state after:
α : Type u_1
inst✝ : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b x : α
hx : ∀ (y : α), y = x
⊢ a = b
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mp.cons_cons.refine_2
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (ix : ℕ),
    (a✝¹ :: l₁✝)[ix]? =
      (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix ↦ if ix = 0 then 0 else (f ix.pred).succ) ⋯) ix]?

Tactic:
rintro ⟨_ | i⟩

Goal state after:
case mp.cons_cons.refine_2.zero
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ (a✝¹ :: l₁✝)[0]? = (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix ↦ if ix = 0 then 0 else (f ix.pred).succ) ⋯) 0]?

case mp.cons_cons.refine_2.succ
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
n✝ : ℕ
⊢ (a✝¹ :: l₁✝)[n✝ + 1]? =
    (a✝¹ :: l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix ↦ if ix = 0 then 0 else (f ix.pred).succ) ⋯) (n✝ + 1)]?
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
⊢ (∃ i, P i) → P p ∨ ∃ i, P (p.succAbove i)

Tactic:
rintro ⟨i, hi⟩
    induction i using p.succAboveCases
    · exact .inl hi
    · exact .inr ⟨_, hi⟩

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1 + 1)
⊢ i.succ.insertNth x (cons a p) j = cons a (i.insertNth x p) j

Tactic:
cases j using Fin.succAboveCases i.succ with
  | x => simp
  | p j =>
    simp only [insertNth_apply_succAbove]
    cases j using Fin.cases <;> simp

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op b a) s

Tactic:
fold_eq_foldl,

Goal state after:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ foldl op b (a ::ₘ s) = fold op (op b a) s
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
head✝ : α
tail✝ : List α
h : Pairwise R (head✝ :: tail✝)
a✝ : Mem a tail✝
⊢ a ∈ tail✝

Tactic:
assumption

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
h : l₁ ≠ l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂

Tactic:
induction l₁ generalizing l₂ <;> rcases l₂ with - | ⟨b, l₂⟩
    · contradiction
    · apply nil
    · exact (not_lt_of_ge H).elim (succ_pos _)
    case cons.cons a l₁ IH =>
      by_cases ab : a = b
      · subst b
        exact .cons <| IH (le_of_succ_le_succ H) (mt (congr_arg _) h)
      · exact .rel ab

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
h : l₁ ≠ l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂

Tactic:
by
    induction l₁ generalizing l₂ <;> rcases l₂ with - | ⟨b, l₂⟩
    · contradiction
    · apply nil
    · exact (not_lt_of_ge H).elim (succ_pos _)
    case cons.cons a l₁ IH =>
      by_cases ab : a = b
      · subst b
        exact .cons <| IH (le_of_succ_le_succ H) (mt (congr_arg _) h)
      · exact .rel ab

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a b : α
⊢ Forall₂ R (a :: l ++ [b]).dropLast (a :: l ++ [b]).tail ↔ Forall₂ R (a :: l) (l ++ [b])

Tactic:
dropLast_concat,

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a b : α
⊢ Forall₂ R (a :: l) (a :: l ++ [b]).tail ↔ Forall₂ R (a :: l) (l ++ [b])
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
x✝ : ¬[] ∈ [l]
⊢ IsChain R [l].flatten ↔
    (∀ (l_1 : List α), l_1 ∈ [l] → IsChain R l_1) ∧
      IsChain (fun l₁ l₂ ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) [l]

Tactic:
by simp [flatten]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons
M : Type u_8
inst✝ : CommMonoid M
m : M
L : List M
ih : IsUnit L.prod → ∀ (m : M), m ∈ L → IsUnit m
h : IsUnit m ∧ IsUnit L.prod
⊢ ∀ (m_1 : M), m_1 ∈ m :: L → IsUnit m_1

Tactic:
exact fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H

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

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
hd : α
tl : List α
⊢ ((hd :: tl).rotate (n + 1)).reverse.rotate (n + 1) = (hd :: tl).reverse

Tactic:
rw [rotate_cons_succ, ← rotate_rotate, hn]
      simp

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

Goal state before:
pp: case zero.zero
⊢ 1 = 0! * (0 + 0 - 1).choose 0

Tactic:
choose_zero_right,

Goal state after:
case zero.zero
⊢ 1 = 0! * 1
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k < n
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

pp: case inr.inl
k : ℕ
⊢ k.choose k = 1 ↔ k = 0 ∨ k = k

pp: case inr.inr
n k : ℕ
hk : n < k
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

Tactic:
· grind [k.choose_mono hk]

Goal state after:
case inr.inl
k : ℕ
⊢ k.choose k = 1 ↔ k = 0 ∨ k = k

case inr.inr
n k : ℕ
hk : n < k
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (s ×ˢ t).Infinite

Tactic:
rintro (h | h)
    · exact h.1.prod_left h.2
    · exact h.1.prod_right h.2

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Group α
a b : α
⊢ (b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹

Tactic:
by
  simp [mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Group α
a b c : α
⊢ b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹

Tactic:
by
  simp [mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ ¬H = ⊥

Tactic:
eq_bot_iff_forall

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ ¬∀ x ∈ H, x = 1
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
n : ℤ
hx✝ : x ^ n ∈ closure {x}
m : ℤ
hy✝ : x ^ m ∈ closure {x}
⊢ ∃ n_1, x ^ n_1 = x ^ n * x ^ m

Tactic:
exact ⟨n + m, zpow_add x n m⟩

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (s ∪ {1}) = closure s

Tactic:
union_singleton,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (insert 1 s) = closure s
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ ↑(map f (comap f H)) = ↑(f.range ⊓ H)

Tactic:
rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
⊢ S = ⊥

Tactic:
eq_bot_iff_forall

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
⊢ ∀ x ∈ S, x = 1
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x : ↥(IsUnit.submonoid M)
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ IsUnit.unit ⋯) x) = x

Tactic:
simp_rw [IsUnit.unit_spec]

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

Goal state before:
pp: case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ < a₂

Tactic:
assumption

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
⊢ (decode₂ α ↑n).isSome = true

Tactic:
obtain ⟨x, hx⟩ := n.2; rw [← hx, encodek₂]; exact rfl

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons.inl
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : f i < g i
⊢ f i * (map f l).prod < g i * (map g l).prod

pp: case cons.inr
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : ∃ a, a ∈ l ∧ f a < g a
⊢ f i * (map f l).prod < g i * (map g l).prod

Tactic:
· exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)

Goal state after:
case cons.inr
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : ∃ a, a ∈ l ∧ f a < g a
⊢ f i * (map f l).prod < g i * (map g l).prod
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ (N.subgroupOf (H ⊔ N)).Normal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer le_sup_right]

Goal state after:
G : Type u_1
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ H ⊔ N ≤ normalizer ↑N
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mpr.inl
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) × α i
i : ι
a : α i
h : r i b.fst
⊢ Lex r s ⟨i, a⟩ b

pp: case mpr.inr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) × α i
a : α b.fst
h : s b.fst (⋯ ▸ a) b.snd
⊢ Lex r s ⟨b.fst, a⟩ b

Tactic:
· exact Lex.left _ _ h

Goal state after:
case mpr.inr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) × α i
a : α b.fst
h : s b.fst (⋯ ▸ a) b.snd
⊢ Lex r s ⟨b.fst, a⟩ b
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mp.left
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
h : Function.swap r i✝ j✝
⊢ Lex r (fun i ↦ Function.swap (s i)) ⟨j✝, b⟩ ⟨i✝, a⟩

pp: case mp.right
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
h : s i✝ a b
⊢ Lex r (fun i ↦ Function.swap (s i)) ⟨i✝, b⟩ ⟨i✝, a⟩

Tactic:
· exact Lex.left _ _ h

Goal state after:
case mp.right
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
h : s i✝ a b
⊢ Lex r (fun i ↦ Function.swap (s i)) ⟨i✝, b⟩ ⟨i✝, a⟩
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mpr.left
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
h : r i✝ j✝
⊢ Lex (Function.swap r) s ⟨j✝, b⟩ ⟨i✝, a⟩

pp: case mpr.right
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
h : Function.swap (s i✝) a b
⊢ Lex (Function.swap r) s ⟨i✝, b⟩ ⟨i✝, a⟩

Tactic:
· exact Lex.left _ _ h

Goal state after:
case mpr.right
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
h : Function.swap (s i✝) a b
⊢ Lex (Function.swap r) s ⟨i✝, b⟩ ⟨i✝, a⟩
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mpr.inl
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) ×' α i
i : ι
a : α i
h : r i b.fst
⊢ Lex r s ⟨i, a⟩ b

pp: case mpr.inr
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) ×' α i
a : α b.fst
h : s b.fst (⋯ ▸ a) b.snd
⊢ Lex r s ⟨b.fst, a⟩ b

Tactic:
· exact Lex.left _ _ h

Goal state after:
case mpr.inr
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) ×' α i
a : α b.fst
h : s b.fst (⋯ ▸ a) b.snd
⊢ Lex r s ⟨b.fst, a⟩ b
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n : M
P : Submonoid M
⊢ powers n ≤ P ↔ n ∈ P

Tactic:
simp [powers_eq_closure]

Goal state after: