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

Goal state before:
pp: case cons.cons
α : Type u_1
head✝¹ : α
tail✝¹ : List α
ih : ∀ {l₁ : List α}, l₁ <+: tail✝¹ → tail✝¹ = l₁ ++ drop l₁.length tail✝¹
head✝ : α
tail✝ : List α
h : head✝ :: tail✝ <+: head✝¹ :: tail✝¹
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝ ++ drop (head✝ :: tail✝).length (head✝¹ :: tail✝¹)

Tactic:
| cons =>

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

Goal state before:
pp: α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
s : Finset α
hs : s.Nonempty
⊢ motive s hs

Tactic:
induction s using Finset.cons_induction with

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ {a}ᶜ = univ.erase a

Tactic:
by
  rw [compl_eq_univ_sdiff, sdiff_singleton_eq_erase]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 1 < ↑(last (n + 1))

Tactic:
val_last,

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ 1 < n + 1
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ ↑(last n) - ↑i = ↑i.rev

Tactic:
val_last,

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ n - ↑i = ↑i.rev
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
hb : b ≠ last n
h : a ≤ b
⊢ ↑(a.castPred ⋯ - b.castPred hb) = ↑(a - b) - 1

Tactic:
by
  obtain (rfl | h') := Fin.eq_or_lt_of_le h
  · simp [val_sub, Nat.sub_add_cancel a.is_le]
  grind [castPred, val_sub_castLT_of_lt]

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

Goal state before:
pp: α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
⊢ #t + #u = #(t ∪ u)

Tactic:
by simp [← card_union_add_card_inter, hstu]

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n ↪ α
⊢ map f univ = { val := ↑(List.ofFn ⇑f), nodup := ⋯ }

Tactic:
by
  simp [Finset.map]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = #s

Tactic:
rw [← subtype_card s H]

Goal state after:
α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = card { x // p x }
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (⇑e.symm ∘ f) ↔ Surjective (⇑e.symm ∘ f)
hsurj : Surjective f
⊢ Injective f

Tactic:
by
    simpa [Function.comp] using e.injective.comp (this.2 (e.symm.surjective.comp hsurj))

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

Goal state before:
pp: case cons_cons
α : Type u_1
l : List α
x : α
l' l₁✝ l₂✝ : List α
y : α
h : l₁✝ <+ l₂✝
IH : x ∈+ l₁✝ → x ∈+ l₂✝
hx : y = x ∧ x ∈ l₁✝ ∨ x ∈+ l₁✝
⊢ y = x ∧ x ∈ l₂✝ ∨ x ∈+ l₂✝

Tactic:
rcases hx with (⟨rfl, hx⟩ | hx)

Goal state after:
case cons_cons.inl
α : Type u_1
l l' l₁✝ l₂✝ : List α
y : α
h : l₁✝ <+ l₂✝
IH : y ∈+ l₁✝ → y ∈+ l₂✝
hx : y ∈ l₁✝
⊢ y = y ∧ y ∈ l₂✝ ∨ y ∈+ l₂✝

case cons_cons.inr
α : Type u_1
l : List α
x : α
l' l₁✝ l₂✝ : List α
y : α
h : l₁✝ <+ l₂✝
IH : x ∈+ l₁✝ → x ∈+ l₂✝
hx : x ∈+ l₁✝
⊢ y = x ∧ x ∈ l₂✝ ∨ x ∈+ l₂✝
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
xₚ yₚ : α p
x y : (j : Fin n) → α (p.succAbove j)
h : p.insertNth xₚ x = p.insertNth yₚ y
i : Fin n
⊢ x i = y i

Tactic:
by simpa using congr_fun h (succAbove p i)

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

Goal state before:
pp: case mpr.refine_1.zero.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨n✝ + 1, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Tactic:
simp [hnm]

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

Goal state before:
pp: case mpr.refine_1.zero.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨n✝ + 1, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

pp: case mpr.refine_1.succ.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ ⟨n✝ + 1, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

pp: case mpr.refine_1.succ.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Tactic:
· simp [hnm]

Goal state after:
case mpr.refine_1.succ.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ ⟨n✝ + 1, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

case mpr.refine_1.succ.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ Finite α

Tactic:
rw [← finite_univ_iff, ← union_compl_self s]

Goal state after:
α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ (s ∪ sᶜ).Finite
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ ¬Fin.find p h < i ↔ ∀ (m : Fin n), m < i → ¬p m

Tactic:
find_lt_iff,

Goal state after:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ (¬∃ m, m < i ∧ p m) ↔ ∀ (m : Fin n), m < i → ¬p m
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
s : Finset γ
hi : Std.IdempotentOp op
⊢ fold op b f (image g s) = fold op b (f ∘ g) s

Tactic:
induction s using Finset.cons_induction with

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

Goal state before:
pp: case refine_2
α : Type u_3
l : List α
R : α → α → Prop
h : ∀ (l' : List α) (h : 1 < l'.length), l' <:+: l → R (l'.head ⋯) (l'.getLast ⋯)
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
⊢ R l[i] l[j]

Tactic:
grind [h _ _ <| List.drop_suffix i _ |>.isInfix.trans <| l.take_prefix (j + 1) |>.isInfix]

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

Goal state before:
pp: case inl
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r a b
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

pp: case inr.inl
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ l₂ l₃ : List α
h : Lex r l₁ l₃
⊢ Lex r (a :: l₁) (a :: l₂) ∨ Lex r (a :: l₂) (a :: l₃)

pp: case inr.inr
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r b a
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

Tactic:
· exact Or.inl (rel ab)

Goal state after:
case inr.inl
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ l₂ l₃ : List α
h : Lex r l₁ l₃
⊢ Lex r (a :: l₁) (a :: l₂) ∨ Lex r (a :: l₂) (a :: l₃)

case inr.inr
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r b a
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝¹ : CommMonoid M
s : Multiset M
inst✝ : DecidableEq M
a : M
⊢ a ^ count a s = (replicate (count a s) a).prod

Tactic:
prod_replicate

Goal state after:
M : Type u_3
inst✝¹ : CommMonoid M
s : Multiset M
inst✝ : DecidableEq M
a : M
⊢ a ^ count a s = a ^ count a s
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case pos
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : a ∈ as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum

Tactic:
simp [dedup_cons_of_mem ha]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : p a = true
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

pp: case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
· refine _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h.symm]) ?_
        simp [hp, count_dedup]

Goal state after:
case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
| (m + n) % l.length

Tactic:
Nat.add_comm m,

Goal state after:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
| (n + m) % l.length
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ IsChain (fun x1 x2 ↦ x1 = x2) (a :: l) ↔ l = replicate l.length a

Tactic:
by
  simp [isChain_eq_iff_eq_replicate, replicate_succ]

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

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ (l.rotate n)[k] = l[(k + n) % l.length]

Tactic:
rw [← Option.some_inj, ← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_rotate]

Goal state after:
α : Type u
l : List α
n k : ℕ
h : k < (l.rotate n).length
⊢ k < l.length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.reverse.rotate n = (l.rotate (l.length - n % l.length)).reverse

Tactic:
by
  rw [← reverse_reverse l]
  simp_rw [reverse_rotate, reverse_reverse, rotate_eq_iff, rotate_rotate, length_rotate,
    length_reverse]
  rw [← length_reverse]
  let k := n % l.reverse.length
  rcases hk' : k with - | k'
  · simp_all! [k, length_reverse, ← rotate_rotate]
  · rcases l with - | ⟨x, l⟩
    · simp
    · rw [Nat.mod_eq_of_lt, Nat.sub_add_cancel, rotate_length]
      · exact Nat.sub_le _ _
      · exact Nat.sub_lt (by simp) (by simp_all! [k])

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

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
f : α → Multiset β
p : β → Prop
inst✝ : DecidablePred p
⊢ filter p (m.bind f) = m.bind fun a ↦ filter p (f a)

Tactic:
by
  simp [bind, filter_join]

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

Goal state before:
pp: n k : ℕ
hk : 0 < k
⊢ (n + 1).choose k = n.choose (k - 1) + n.choose k

Tactic:
obtain ⟨l, rfl⟩ : ∃ l, k = l + 1 := Nat.exists_eq_add_of_le' hk

Goal state after:
n l : ℕ
hk : 0 < l + 1
⊢ (n + 1).choose (l + 1) = n.choose (l + 1 - 1) + n.choose (l + 1)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ n.choose k = (n - 1).choose (k - 1) + (n - 1).choose k

Tactic:
obtain ⟨l, rfl⟩ : ∃ l, k = l + 1 := Nat.exists_eq_add_of_le' hk

Goal state after:
n : ℕ
hn : 0 < n
l : ℕ
hk : 0 < l + 1
⊢ n.choose (l + 1) = (n - 1).choose (l + 1 - 1) + (n - 1).choose (l + 1)
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
⊢ ((if c = a then count b l else 0) + if c = b then count a l else 0) +
      (count a l * count b l - if a = b then count a l else 0) =
    (count a l + if c = a then 1 else 0) * (count b l + if c = b then 1 else 0) -
      if a = b then count a l + if c = a then 1 else 0 else 0

Tactic:
have := Nat.le_mul_self (count c l)

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
H₂ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0
this : count c l ≤ count c l * count c l
⊢ ((if c = a then count b l else 0) + if c = b then count a l else 0) +
      (count a l * count b l - if a = b then count a l else 0) =
    (count a l + if c = a then 1 else 0) * (count b l + if c = b then 1 else 0) -
      if a = b then count a l + if c = a then 1 else 0 else 0
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq α
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) → i ∈ s

Tactic:
simp +contextual [mem_image]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq β
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) → i ∈ t

Tactic:
simp +contextual [mem_image]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
inst✝ : DecidablePred p
⊢ {x ∈ s ×ˢ t | p x.1} = filter p s ×ˢ t

Tactic:
by
  simpa using filter_product p fun _ => true

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Finset β
a x : α
y : β
⊢ (x, y) ∈ {a} ×ˢ t ↔ (x, y) ∈ map { toFun := Prod.mk a, inj' := ⋯ } t

Tactic:
simp [and_left_comm, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ {b} ↔ (x, y) ∈ map { toFun := fun i ↦ (i, b), inj' := ⋯ } s

Tactic:
simp [and_left_comm, eq_comm]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ f (b * ↑c) = f b * f ↑c

Tactic:
f.map_mul

Goal state after:
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ f b * f ↑c = f b * f ↑c
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
⊢ ∀ {a b : M}, a ∈ Set.ofPred IsUnit → b ∈ Set.ofPred IsUnit → a * b ∈ Set.ofPred IsUnit

Tactic:
by
    intro a b ha hb
    rw [Set.mem_ofPred_eq] at *
    exact IsUnit.mul ha hb

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H K : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ map f (H ⊓ K) = map f H ⊓ map f K

Tactic:
rw [← SetLike.coe_set_eq]
  simp [Set.image_inter hf]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
N : Type u_5
P : Type u_6
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x : G
hx : f x = 1
⊢ f x⁻¹ = f x * f x⁻¹

Tactic:
by rw [hx, one_mul]

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

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ z ∈ closure {x, y} ↔ ∃ m n, x ^ m * y ^ n = z

Tactic:
rw [← Set.singleton_union, Subgroup.closure_union, mem_sup]
  simp_rw [mem_closure_singleton, exists_exists_eq_and]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
x✝ : (fun x ↦ x ∈ Set.range encode) x
n : α
hn : encode n = x
⊢ (some n).isSome = true

Tactic:
exact rfl

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)
x : α
hx : encode x = ↑n
⊢ (some x).isSome = true

Tactic:
exact rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
⊢ DecidableEq (ULower α)

Tactic:
by
  delta ULower; exact Encodable.decidableEqOfEncodable _

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x

Tactic:
rw [conjugatesOfSet, Set.mem_iUnion₂]
  simp only [conjugatesOf, isConj_iff, Set.mem_ofPred_eq, exists_prop]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f (f_inv (x * y)) = f (f_inv x * f_inv y)

Tactic:
f.map_mul

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f (f_inv (x * y)) = f (f_inv x) * f (f_inv y)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons.left
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * tail✝.prod

pp: case cons.right
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * tail✝.prod

Tactic:
case cons.left => exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)

Goal state after:
case cons.right
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * tail✝.prod
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) < (a₁, b₂)
⊢ toLex (a₁, b₁) < toLex (a₁, b₂)

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
ha : (a₁, b₁).1 < (a₂, b₂).1
⊢ toLex (a₁, b₁) < toLex (a₂, b₂)

Tactic:
· exact right _ (Prod.mk_lt_mk_iff_right.1 h)

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
ha : (a₁, b₁).1 < (a₂, b₂).1
⊢ toLex (a₁, b₁) < toLex (a₂, b₂)
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: case h.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 < y.1
⊢ ∃ a, toLex x < a ∧ a < toLex y

pp: case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y

Tactic:
· obtain ⟨v, hv⟩ := exists_lt y.2
      use toLex (y.1, v)
      simp [Prod.Lex.toLex_lt_toLex, h, hv]

Goal state after:
case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = s ⊔ mrange t.subtype

Tactic:
mrange_subtype

Goal state after:
N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = s ⊔ t
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ y :: l
⊢ a ≤ foldr max b (y :: l)

Tactic:
simp only [List.foldr]
    obtain rfl | hl := mem_cons.mp hx
    · exact le_max_of_le_left h
    · exact le_max_of_le_right (IH hl)

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

Goal state before:
pp: α : Type u
⊢ sublistsAux = fun a r ↦ (Array.foldl (fun r l ↦ (r.push l).push (a :: l)) #[] r.toArray).toList

Tactic:
by
  funext a r
  simp only [sublistsAux]
  have := foldl_hom Array.toList (g₁ := fun r l => (r.push l).push (a :: l))
    (g₂ := fun r l => r ++ [l, a :: l]) (l := r) (init := #[]) (by simp)
  simpa using this

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

Goal state before:
pp: case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
H : (image f s).max' hne ∈ image f s
⊢ motive s

Tactic:
simp only [mem_image] at H

Goal state after:
case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
H : ∃ a ∈ s, f a = (image f s).max' hne
⊢ motive s
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (do
      let x ← l.sublists
      map (fun x_1 ↦ x_1 ++ x) [a].sublists) =
    do
    let x ← l.sublists
    [x, a :: x]

Tactic:
simp only [sublists_singleton, map_cons, bind_eq_flatMap, nil_append, cons_append, map_nil]

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

Goal state before:
pp: case cons
α : Type u
hd : α
tl : List α
ih : tl.reverse.sublists = map reverse tl.sublists'
⊢ (hd :: tl).reverse.sublists = map reverse (hd :: tl).sublists'

Tactic:
simp only [reverse_cons, sublists_append, sublists'_cons, map_append, ih, sublists_singleton,
      bind_eq_flatMap, map_map, flatMap_cons, append_nil, flatMap_nil, Function.comp_def]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
⊢ s.sup (f ⊔ g) = s.sup f ⊔ s.sup g

Tactic:
induction s using Finset.cons_induction with

Goal state after: