mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ snoc (fun j ↦ cast ⋯ (p j)) x j.castSucc ≍ (last n).removeNth (snoc (fun j ↦ cast ⋯ (p j)) x) j

Tactic:
apply congr_arg_heq

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ j.castSucc = (last n).succAbove j
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
t : Set α
ht : t ⊆ s
⊢ t.Finite

Tactic:
have := hs.to_subtype
  exact Finite.Set.subset _ ht

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Antisymm r
x : α
hx : x ∈ []
hxs : Pairwise r []
⊢ orderedInsert r x ([].erase x) = []

Tactic:
grind +splitIndPred

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : Std.Antisymm r
x head✝ : α
tail✝ : List α
tail_ih✝ : x ∈ tail✝ → Pairwise r tail✝ → orderedInsert r x (tail✝.erase x) = tail✝
hx : x ∈ head✝ :: tail✝
hxs : Pairwise r (head✝ :: tail✝)
⊢ orderedInsert r x ((head✝ :: tail✝).erase x) = head✝ :: tail✝

Tactic:
grind +splitIndPred

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

Goal state before:
pp: case neg.inr
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
b' : α
bm✝ : b' ∈ List.orderedInsert r a l
bm : b' ∈ l
⊢ r b b'

Tactic:
· exact rel_of_pairwise_cons h bm

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → ∀ (d : List α), d ~ c → d <+ tail✝ → c <+ insertionSort r tail✝
c : List α
hs : Pairwise r c
d : List α
hc : d ~ c
hd : d <+ a :: tail✝
⊢ c <+ insertionSort r (a :: tail✝)

Tactic:
cases hd with
    | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
      have hm := hc.mem_iff.mp <| mem_cons_self ..
      have he := orderedInsert_erase _ _ hm hs
      exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)

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

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
k : Fin n
⊢ m (j.succAbove (i.succAbove k)) ≍ m ((j.succAbove i).succAbove ((i.predAbove j).succAbove k))

Tactic:
apply congr_arg_heq

Goal state after:
n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
k : Fin n
⊢ j.succAbove (i.succAbove k) = (j.succAbove i).succAbove ((i.predAbove j).succAbove k)
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_3
l : List α
R : α → α → Prop
⊢ Pairwise R l ↔ ∀ (l' : List α) (h : 1 < l'.length), l' <:+: l → R (l'.head ⋯) (l'.getLast ⋯)

Tactic:
refine l.pairwise_iff_getElem.trans ⟨fun h l' hne ⟨l₁, l₂, hl⟩ ↦ ?_, fun h i j hi hj hij ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_3
l : List α
R : α → α → Prop
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
l' : List α
hne : 1 < l'.length
x✝ : l' <:+: l
l₁ l₂ : List α
hl : l₁ ++ l' ++ l₂ = l
⊢ R (l'.head ⋯) (l'.getLast ⋯)

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]
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l.tail
⊢ R (l.head ⋯) a

Tactic:
grind +splitIndPred

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l
hhead : R (l.head ⋯) (l.head ⋯)
⊢ R (l.head ⋯) a

Tactic:
grind +splitIndPred

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ : List α
hab : ¬Lex r (a :: l₁) (b :: l₂)
hba : ¬Lex r (b :: l₂) (a :: l₁)
⊢ a :: l₁ = b :: l₂

Tactic:
by
      obtain rfl := Std.Trichotomous.trichotomous a b (mt rel hab) (mt rel hba)
      rw [aux l₁ l₂ (mt cons hab) (mt cons hba)]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
h : IsChain R l
⊢ IsChain R l.tail

Tactic:
grind +splitIndPred

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
x : α
l : List α
l_ne_nil : l ≠ []
hl : IsChain R l
h : R x (l.head l_ne_nil)
⊢ IsChain R (x :: l)

Tactic:
grind +splitIndPred

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

Goal state before:
pp: case nil
α : Type u_1
p : α → Prop
r : { a // p a } → { a // p a } → Prop
h : ∀ (x : α), x ∈ [] → p x
⊢ IsChain r ([].attachWith p h) ↔ IsChain (fun a b ↦ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) []

Tactic:
grind +splitIndPred

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Prop
r : { a // p a } → { a // p a } → Prop
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (h : ∀ (x : α), x ∈ tail✝ → p x),
    IsChain r (tail✝.attachWith p h) ↔ IsChain (fun a b ↦ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) tail✝
h : ∀ (x : α), x ∈ head✝ :: tail✝ → p x
⊢ IsChain r ((head✝ :: tail✝).attachWith p h) ↔ IsChain (fun a b ↦ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) (head✝ :: tail✝)

Tactic:
grind +splitIndPred

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

Goal state before:
pp: α : 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)
        (match true with
        | true => a :: filter p as.dedup
        | false => filter p as.dedup)).sum =
    (map (fun i ↦ count i as) (filter p as.dedup)).sum

Tactic:
| =>

Goal state after:
α : 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)
        (match true with
        | true => a :: filter p as.dedup
        | false => filter p as.dedup)).sum =
    (map (fun i ↦ count i as) (filter p as.dedup)).sum
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: α : 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)
        (match false with
        | true => a :: filter p as.dedup
        | false => filter p as.dedup)).sum =
    (map (fun i ↦ count i as) (filter p as.dedup)).sum

Tactic:
| =>

Goal state after:
α : 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)
        (match false with
        | true => a :: filter p as.dedup
        | false => filter p as.dedup)).sum =
    (map (fun i ↦ count i as) (filter p as.dedup)).sum
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate n ~ l

Tactic:
rw [rotate_eq_rotate']
  induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · rw [rotate'_cons_succ]
      exact (hn _).trans (perm_append_singleton _ _)

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
⊢ a ∣ l.prod

Tactic:
let ⟨s, t, h⟩ := append_of_mem ha
  rw [h, prod_append, prod_cons, mul_left_comm]
  exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_2.e_a
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • {a}) = n • if p a then {a} else 0

Tactic:
split_ifs with hp <;>
      · simp only [filter_eq_self, nsmul_zero, filter_eq_nil]
        intro b hb
        rwa [mem_singleton.mp (mem_of_mem_nsmul hb)]

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

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ ↑⟨k, hk⟩ = ↑⟨((l.length - n % l.length + k) % l.length + n) % l.length, ⋯⟩

Tactic:
simp only [mod_add_mod]

Goal state after:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k = (l.length - n % l.length + k + n) % l.length
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
m : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p m = m.bind fun a ↦ if p a then {a} else 0

Tactic:
induction m using Multiset.induction with

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

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
f : α → Option β
⊢ filterMap f m = m.bind fun a ↦ (Option.map singleton (f a)).getD 0

Tactic:
induction m using Multiset.induction with

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

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ l.cyclicPermutations.length = l.length

Tactic:
simp [cyclicPermutations_of_ne_nil _ h]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
h : l₁ ~ l₂
⊢ l₁.offDiag ~ l₂.offDiag

Tactic:
classical simp_all [perm_iff_count, count_offDiag_eq_mul_sub_ite]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α ↪ β
g : γ ↪ δ
s : Finset α
t : Finset γ
⊢ map (f.prodMap g) (s ×ˢ t) = map f s ×ˢ map g t

Tactic:
simpa [← coe_inj] using Set.prodMap_image_prod f g s t

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

Goal state before:
pp: n a b : ℕ
h : n = a + b
this : (a + b).choose (a + b - b) = (a + b).choose b
⊢ n.choose a = n.choose b

Tactic:
Nat.add_sub_cancel_right

Goal state after:
n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
⊢ n.choose a = n.choose b
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
have e : (n + 1) * choose n k = choose n (k + 1) * (k + 1) + choose n k * (k + 1) := by
    rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, add_one_mul_choose_eq]

Goal state after:
n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
⊢ n.choose (k + 1) * (k + 1) = n.choose k * (n - k)
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
have : n + (k + 1) < (n + 1) + (k + 1) := Nat.add_lt_add_right (Nat.lt_succ_self _) _

Goal state after:
n k : ℕ
this : n + (k + 1) < n + 1 + (k + 1)
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
⊢ IsConj a b

Tactic:
by
    have ha := mem_conjugatesOf_self (a := b)
    rwa [← h] at ha

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
hf : Bijective f
s : (i : ι) → κ i → Set α
⊢ f '' ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, f '' s i j

Tactic:
by simp_rw [image_iInter hf]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x⁻¹) ↔ ∃ x, x ∈ H ∧ P x

Tactic:
by
  constructor <;>
    · rintro ⟨x, x_in, hx⟩
      exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
one_mem : 1 ∈ s
x : G
hx : x ∈ s
⊢ x⁻¹ ∈ s

Tactic:
simpa using hs 1 one_mem x hx

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

Goal state before:
pp: F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : InjOn ⇑f ↑s
a : G
ha : a ∈ s
ha' : f a = 1
⊢ a = 1

Tactic:
by
    refine h ha (one_mem s) ?_
    rwa [map_one]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
k : Set G
p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : x ∈ closure k), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : x ∈ closure k), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : x ∈ closure k
hy : y ∈ closure k
⊢ p x y hx hy

Tactic:
by
  induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem _ _ h hz
    | one => exact one_left _ (subset_closure hz)
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | inv _ _ h => exact inv_left _ _ _ _ h
  | one => exact one_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂
  | inv _ _ h => exact inv_right _ _ _ _ h

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
⊢ y ∈ closure {x} ↔ ∃ n, x ^ n = y

Tactic:
refine
    ⟨fun hy => closure_induction ?_ ?_ ?_ ?_ hy, fun ⟨n, hn⟩ =>
      hn ▸ zpow_mem (subset_closure <| mem_singleton x) n⟩
  · intro y hy
    rw [eq_of_mem_singleton hy]
    exact ⟨1, zpow_one x⟩
  · exact ⟨0, zpow_zero x⟩
  · rintro _ _ _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    exact ⟨n + m, zpow_add x n m⟩
  rintro _ _ ⟨n, rfl⟩
  exact ⟨-n, zpow_neg x n⟩

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

Goal state before:
pp: case refine_1.refine_3
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i✝ : ι
hp : p i✝
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x✝ : G
hx : x✝ ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
x y : G
hx✝ : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
hy✝ : y ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
i : ι
hip : p i
hi : x ∈ K i
j : ι
hjp : p j
hj : y ∈ K j
k : ι
hk : k ∈ {i | p i}
hki : ((fun x1 x2 ↦ x1 ≤ x2) on K) i k
hkj : ((fun x1 x2 ↦ x1 ≤ x2) on K) j k
⊢ ∃ i, p i ∧ x * y ∈ K i

Tactic:
exact ⟨k, hk, mul_mem (hki hi) (hkj hj)⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : G
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
by simp [mem_iSup_of_directed hS]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B

Tactic:
refine
    map_injective_of_ker_le B.subtype (ker_le_comap _ _)
      (le_trans (ker_le_comap B.subtype _) le_sup_left) ?_
  simp only [subgroupOf, map_comap_eq, map_sup, range_subtype]
  rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ (normalizer ↑H).unop = normalizer ↑H.unop

Tactic:
rw [← op_inj, op_unop, op_normalizer, op_unop]

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

Goal state before:
pp: m n : ℕ
⊢ m * (2 ^ n * 2) = 2 ^ (n + 1) * m

Tactic:
← Nat.pow_succ

Goal state after:
m n : ℕ
⊢ m * 2 ^ n.succ = 2 ^ (n + 1) * m
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
N : Type u_3
inst✝ : Group N
g : G
⊢ ∀ {x : G}, (x ∈ Set.range fun x ↦ g ^ x) → x⁻¹ ∈ Set.range fun x ↦ g ^ x

Tactic:
by rintro _ ⟨a, rfl⟩; exact ⟨-a, zpow_neg ..⟩

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

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
by simp [mem_iSup_of_directed hS]

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

Goal state before:
pp: 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

Tactic:
exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)

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

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

Tactic:
| h x
     => 

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
y : Lex (α × β)
x : α × β
h : toLex x < y
⊢ ∃ a, toLex x < a ∧ a < y
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
y : Lex (α × β)
x : α × β
h : toLex x < y
⊢ ∃ a, toLex x < a ∧ a < y

Tactic:
| h x
     => 

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
y : Lex (α × β)
x : α × β
h : toLex x < y
⊢ ∃ a, toLex x < a ∧ a < y
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : Monoid M
a : M
inst✝ : DecidableEq M
n : M
h : Function.Injective fun m ↦ n ^ m
x✝¹ x✝ : Multiplicative ℕ
⊢ pow n (Multiplicative.toAdd (x✝¹ * x✝)) = pow n (Multiplicative.toAdd x✝¹) * pow n (Multiplicative.toAdd x✝)

Tactic:
by simp only [pow, map_mul, ofAdd_add, toAdd_mul]

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

Goal state before:
pp: case append_singleton.some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
ho : (Option.casesOn (some c) (some a) fun c ↦ if r a c then some a else some c) = some m
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m

Tactic:
grind +splitIndPred

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ ofNat β n = e.symm (ofNat α n)

Tactic:
refine ofNat_of_decode ?_

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ decode n = some (e.symm (ofNat α n))
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ u.toLeft.disjSum u.toRight = u

Tactic:
ext (x | x) <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
⊢ s.disjSum t ⊆ u ↔ s ⊆ u.toLeft ∧ t ⊆ u.toRight

Tactic:
by simp [subset_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
⊢ u ⊆ s.disjSum t ↔ u.toLeft ⊆ s ∧ u.toRight ⊆ t

Tactic:
by simp [subset_iff]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Countable α
inst✝² : Infinite α
inst✝¹ : Countable β
inst✝ : Infinite β
⊢ Nonempty (α ≃ β)

Tactic:
cases nonempty_denumerable α
  cases nonempty_denumerable β
  exact ⟨(Denumerable.eqv _).trans (Denumerable.eqv _).symm⟩

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : Top α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ ⊤ ⊔ ⊤ = ⊤

Tactic:
sup_top_eq

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : Top α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
f✝ g✝ f g : TopHom α β
⊢ ⊤ = ⊤
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Lattice α
inst✝⁵ : Lattice β
inst✝⁴ : FunLike F α β
inst✝³ : OrderBot α
inst✝² : OrderBot β
inst✝¹ : BotHomClass F α β
inst✝ : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
⊢ Disjoint (f a) (f b)

Tactic:
by
  rw [disjoint_iff, ← map_inf, h.eq_bot, map_bot]

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.revzip.reverse.unzip.fst.zip l.revzip.reverse.unzip.snd = l.reverse.revzip

Tactic:
simp [unzip_eq_map, revzip, map_reverse, map_fst_zip, map_snd_zip]

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

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
IH : sublistsLen (n + 1) l₁✝ <+ sublistsLen (n + 1) l₂✝
⊢ sublistsLen (n + 1) l₁✝ <+ sublistsLen (n + 1) (a :: l₂✝)

Tactic:
refine IH.trans ?_
    rw [sublistsLen_succ_cons]
    apply sublist_append_left

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

Goal state before:
pp: case succ.cons_cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : sublistsLen (n + 1) l₁✝ <+ sublistsLen (n + 1) l₂✝
⊢ sublistsLen (n + 1) (a :: l₁✝) <+ sublistsLen (n + 1) (a :: l₂✝)

Tactic:
| cons_cons a s IH =>

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

Goal state before:
pp: case cons_cons
α : Type u
l l' l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : l₁✝ ∈ sublistsLen l₁✝.length l₂✝
⊢ a :: l₁✝ ∈ sublistsLen (a :: l₁✝).length (a :: l₂✝)

Tactic:
| cons_cons a s IH =>

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
y : Finset α
hyt : y ⊆ t \ s
hyn : #y = n - #s
⊢ #(y ∪ s) = n

Tactic:
card_union_of_disjoint (disjoint_of_subset_left hyt disjoint_sdiff_self_left),

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
y : Finset α
hyt : y ⊆ t \ s
hyn : #y = n - #s
⊢ #y + #s = n
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case refine_1
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
⊢ a ∈ (range (#s + 1)).disjiUnion (fun i ↦ powersetCard i s) ⋯

Tactic:
rw [mem_disjiUnion]
    exact
      ⟨a.card, mem_range.mpr (Nat.lt_succ_of_le (card_le_card (mem_powerset.mp ha))),
        mem_powersetCard.mpr ⟨mem_powerset.mp ha, rfl⟩⟩

Goal state after: