mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁺ᵐ * a⁻ᵐ⁻¹ ⊓ a⁻ᵐ * a⁻ᵐ⁻¹ = a⁻ᵐ⁻¹

Tactic:
mul_inv_cancel,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁺ᵐ * a⁻ᵐ⁻¹ ⊓ 1 = a⁻ᵐ⁻¹
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inl
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : n < m
⊢ n = m

pp: case inr.inl
n : ℕ
hn : 1 < n
h : n ! = n !
⊢ n = n

pp: case inr.inr
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m < n
⊢ n = m

Tactic:
· rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm
    cases lt_irrefl _ hnm

Goal state after:
case inr.inl
n : ℕ
hn : 1 < n
h : n ! = n !
⊢ n = n

case inr.inr
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m < n
⊢ n = m
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n ! * (n + 1).ascFactorial 0 = (n + 0)!

Tactic:
rw [ascFactorial_zero, Nat.add_zero, Nat.mul_one]

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

Goal state before:
pp: case inr
n k j : ℕ
hn : n > 0
⊢ (n + j) * n.ascFactorial j ≤ (j + 1) * n * (j ! * n ^ j)

Tactic:
refine Nat.mul_le_mul ?_ (ascFactorial_le_factorial_mul_pow n j)

Goal state after:
case inr
n k j : ℕ
hn : n > 0
⊢ n + j ≤ (j + 1) * n
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
H : ⌊2 * fract x⌋ = 1
this : 0 < fract x
⊢ ⌈fract x⌉ = (⌊2 * fract x⌋ + 1) / 2

Tactic:
by simp [this, H, ceil_eq_iff, (fract_lt_one _).le]

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

Goal state before:
pp: m k : ℕ+
⊢ ↑(m.mod k) + m.div k * ↑k = ↑m

Tactic:
rw [mul_comm]

Goal state after:
m k : ℕ+
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m k : ℕ+
⊢ m.div k * ↑k + ↑(m.mod k) = ↑m

Tactic:
rw [mul_comm]

Goal state after:
m k : ℕ+
⊢ ↑k * m.div k + ↑(m.mod k) = ↑m
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
⊢ fract 0 = 0

Tactic:
by rw [fract, floor_zero, cast_zero, sub_self]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
let s : Set ℤ := { n : ℤ | a ^ n ≤ g }

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddCommMonoid G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℕ
x : G
⊢ f (x + n • a) = f x + n • b

Tactic:
map_add_nsmul

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddCommMonoid G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℕ
x : G
⊢ f x + n • b = f x + n • b
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ m, y ^ m ≤ x
M : ℕ
hM : x < y ^ M
⊢ ∃ b, ∀ (m : ℤ), y ^ m ≤ x → m ≤ b

Tactic:
refine ⟨M, fun m hm ↦ ?_⟩

Goal state after:
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ m, y ^ m ≤ x
M : ℕ
hM : x < y ^ M
m : ℤ
hm : y ^ m ≤ x
⊢ m ≤ ↑M
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ m, y ^ m ≤ x
hb : ∃ b, ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he

Goal state after:
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ m, y ^ m ≤ x
hb : ∃ b, ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
n : ℤ
hn₁ : y ^ n ≤ x
hn₂ : ∀ (z : ℤ), y ^ z ≤ x → z ≤ n
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))
Module: Mathlib.Algebra.Group.Action.Units

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ (g * g⁻¹) • 1 = 1

Tactic:
mul_inv_cancel,

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
α : Type u_5
inst✝⁴ : Group G
inst✝³ : Monoid M
inst✝² : MulAction G M
inst✝¹ : SMulCommClass G M M
inst✝ : IsScalarTower G M M
g : G
m : Mˣ
⊢ 1 • 1 = 1
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p : P
⊢ {p} /ₛ {p} = {1}

Tactic:
Set.singleton_sdiv_singleton,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p : P
⊢ {p /ₛ p} = {1}
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
⊢ -(y -ᵥ (pointReflection x) y) = -(2 • (y -ᵥ x))

Tactic:
by simp [← neg_nsmul]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : List α
h : t ⊆ s
⊢ (↑(s ++ t)).dedup = ↑s.dedup

Tactic:
← coe_add,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : List α
h : t ⊆ s
⊢ (↑s + ↑t).dedup = ↑s.dedup
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → ¬(p a ∧ ¬p a)

Tactic:
simp [-Bool.not_eq_true, -not_and]

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

Goal state before:
pp: α : Type u_1
β : Type v
p : α → Prop
inst✝¹ : DecidablePred p
f : α → β
hf : Injective f
s : Multiset α
inst✝ : DecidablePred fun b ↦ ∃ a, p a ∧ f a = b
⊢ map f (filter p s) = filter (fun b ↦ ∃ a, p a ∧ f a = b) (map f s)

Tactic:
simp [filter_map, hf.eq_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x : α
⊢ replicate (min n (count x s)) x = replicate (min (count x s) n) x

Tactic:
min_comm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x : α
⊢ replicate (min (count x s) n) x = replicate (min (count x s) n) x
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
m : a ∈ s
⊢ filter p (s.erase a) = filter p (a ::ₘ s.erase a)

Tactic:
by rw [filter_cons_of_neg _ h]

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

Goal state before:
pp: n : ℕ
⊢ ↑(List.range n ++ [n]) = n ::ₘ range n

Tactic:
← coe_add,

Goal state after:
n : ℕ
⊢ ↑(List.range n) + ↑[n] = n ::ₘ range n
Module: Mathlib.Data.Multiset.Range

Goal state before:
pp: a : ℕ
m : Multiset ℕ
⊢ _root_.Disjoint (range a) (map (fun x ↦ a + x) m)

Tactic:
rw [disjoint_left]
  intro x hxa hxb
  rw [range, mem_coe, List.mem_range] at hxa
  obtain ⟨c, _, rfl⟩ := mem_map.1 hxb
  exact (Nat.le_add_right _ _).not_gt hxa

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
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
rw [succAbove_of_succ_le _ _ h,
      succAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), rev_succ, rev_rev]

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

Goal state before:
pp: n m✝ m : ℕ
a b : Fin n
⊢ (fun x ↦ x.addNat m) a = (fun x ↦ x.addNat m) b → a = b

Tactic:
by simp [Fin.ext_iff]

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

Goal state before:
pp: n✝ m✝ n m : ℕ
a b : Fin m
⊢ natAdd n a = natAdd n b → a = b

Tactic:
by simp [Fin.ext_iff]

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

Goal state before:
pp: case pos
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : 1 ≠ i ∧ 1 ≠ j
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

pp: case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

Tactic:
· exact ⟨⟨1, by lia⟩, h1⟩

Goal state after:
case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a.succ = b.succ → a = b

Tactic:
by simp [Fin.ext_iff]

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

Goal state before:
pp: n m : ℕ
a b : Fin m
⊢ castAdd n a = castAdd n b ↔ a = b

Tactic:
by simp [Fin.ext_iff]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s ∪ t) = #s + #t ↔ Disjoint s t

Tactic:
rw [← card_union_add_card_inter]; simp [disjoint_iff_inter_eq_empty]

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

Goal state before:
pp: n : ℕ
j : Fin n
⊢ succAbove 1 j.succ = j.succ.succ

Tactic:
by
  have := succ_succAbove_succ 0 j; rwa [succ_zero_eq_one, zero_succAbove] at this

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

Goal state before:
pp: n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
⊢ g ∘ cons y q = cons (g y) (g ∘ q)

Tactic:
ext j
  by_cases h : j = 0
  · rw [h]
    rfl
  · let j' := pred j h
    have : j'.succ = j := succ_pred j h
    rw [← this, cons_succ, comp_apply, comp_apply, cons_succ]

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

Goal state before:
pp: case refine_1.refine_1
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
ll : Fin m
⊢ a ll = append a (append b c) (Fin.cast ⋯ (castAdd p (castAdd n ll)))

Tactic:
simp [castAdd_castAdd]

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

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : j = i
⊢ init (update q i.castSucc y) j = update (init q) i y j

Tactic:
rw [h]
    simp [init]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
g : (j : Fin (n + 1)) → α j
⊢ p.insertNth a f = g ↔ a = g p ∧ f = p.removeNth g

Tactic:
by
  simp [funext_iff, forall_iff_succAbove p, removeNth]

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

Goal state before:
pp: case neg
α : 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
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
suffices ∀ b' : α, b' ∈ List.orderedInsert r a l → r b b' by
        simpa [orderedInsert_cons, h', h.of_cons.orderedInsert a l]
      intro b' bm
      rcases (mem_orderedInsert r).mp bm with rfl | bm
      · exact (total_of r _ _).resolve_left h'
      · exact rel_of_pairwise_cons h bm

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

Goal state before:
pp: case cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a : α
tail✝ c : List α
ih : c.erase a <+ insertionSort r tail✝
hs : Pairwise r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
⊢ c <+ insertionSort r (a :: tail✝)

Tactic:
have hm := hc.mem_iff.mp <| mem_cons_self ..

Goal state after:
case cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a : α
tail✝ c : List α
ih : c.erase a <+ insertionSort r tail✝
hs : Pairwise r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
hm : a ∈ c
⊢ c <+ insertionSort r (a :: tail✝)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ (range f).Infinite

Tactic:
← image_univ,

Goal state after:
α : Type u
β : Type v
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ (f '' univ).Infinite
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑j < ↑k
⊢ (if ↑k < ↑j then g k.castSucc else if ↑k = ↑j then op (g k.castSucc) (g k.succ) else g k.succ) = g k.succ

Tactic:
if_neg (not_lt_of_gt h),

Goal state after:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑j < ↑k
⊢ (if ↑k = ↑j then op (g k.castSucc) (g k.succ) else g k.succ) = g k.succ
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
H₁ : ∀ (x : α), x ∈ l → R x x
H₂ : Pairwise R l
⊢ Pairwise (flip R) l

Tactic:
rwa [Std.Symm.flip_eq]

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

Goal state before:
pp: case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (map (map fun x ↦ a + x) l.ranges)

Tactic:
pairwise_map

Goal state after:
case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise (fun a_1 b ↦ (map (fun x ↦ a + x) a_1).Disjoint (map (fun x ↦ a + x) b)) l.ranges
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ (l ++ [a]).length

Tactic:
rw [length_append, length_cons, List.length]

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ l.length + (0 + 1)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ (take (n % (a :: l).length) (a :: l)).prod *
      ((drop (n % (a :: l).length) (a :: l)).prod * (drop (n % (a :: l).length) (a :: l)).prod⁻¹) =
    (take (n % (a :: l).length) (a :: l)).prod

Tactic:
mul_inv_cancel,

Goal state after:
G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ (take (n % (a :: l).length) (a :: l)).prod * 1 = (take (n % (a :: l).length) (a :: l)).prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (tl ++ [hd]).rotate' n ~ hd :: tl

Tactic:
exact (hn _).trans (perm_append_singleton _ _)

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
⊢ (map (fun x ↦ count x l) l.dedup).sum = l.length

Tactic:
by
  simpa using sum_map_count_dedup_filter_eq_countP (fun _ => True) l

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

Goal state before:
pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ l[m - (l.length - n % l.length)]? = l[(m + n) % l.length]?

pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length

Tactic:
· congr 1
      rw [length_drop] at hm
      have hm' := Nat.sub_le_iff_le_add'.1 hm
      have : n % length l + m - length l < length l := by
        rw [Nat.sub_lt_iff_lt_add hm']
        exact Nat.add_lt_add hlt hml
      conv_rhs => rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
      lia

Goal state after:
case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case e'_2
ι : Type u_2
G : Type u_4
inst✝ : DivisionCommMonoid G
m : Multiset ι
f : ι → G
n : ℤ
⊢ map (fun i ↦ f i ^ n) m = map (⇑(zpowGroupHom n)) (map f m)

Tactic:
simp only [map_map, Function.comp_apply, zpowGroupHom_apply]

Goal state after:
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst✝ : Nonempty β
f : ((i : ι) → α i) → β
s : Set ι
⊢ DependsOn f s ↔ ∃ g, f = g ∘ s.domRestrict

Tactic:
rw [dependsOn_iff_factorsThrough, factorsThrough_iff]

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

Goal state before:
pp: α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((insert a s).pi t).val = ((t a).biUnion fun b ↦ image (Pi.cons s a b) (s.pi t)).val

Tactic:
← (pi (insert a s) t).2.dedup

Goal state after:
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((insert a s).pi t).val.dedup = ((t a).biUnion fun b ↦ image (Pi.cons s a b) (s.pi t)).val
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
cases n
  · cases k
    · rw [ascFactorial_zero, choose_zero_right, factorial_zero, Nat.mul_one]
    · simp only [zero_ascFactorial, Nat.zero_add, succ_sub_succ_eq_sub,
        Nat.sub_zero, choose_succ_self, Nat.mul_zero]
  rw [ascFactorial_eq_factorial_mul_choose]
  simp only [succ_add_sub_one]

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α : Type u_2
I : Type u
f✝ : I → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I
η : Type v
R : Type w
s : ι → η
inst✝ : MulOneClass R
f g : ι → R
⊢ extend s (f * g) 1 = extend s f 1 * extend s g 1

Tactic:
simpa using Function.extend_mul s f g 1 1

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Mul α
inst✝ : IsRightCancelMul α
s t : Set α
⊢ s.Nontrivial → t.Nonempty → (s * t).Nontrivial

Tactic:
rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩
  exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
b : α
⊢ (fun x ↦ x * b) ⁻¹' 1 = {b⁻¹}

Tactic:
rw [← image_mul_right', image_one, one_mul]

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

Goal state before:
pp: case a.mul
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x hx✝ : M
y : x ∈ closure s
hy✝ : hx✝ ∈ closure s
hx : x ∈ {1} ∪ ↑(Subsemigroup.closure s)
hy : hx✝ ∈ {1} ∪ ↑(Subsemigroup.closure s)
⊢ x * hx✝ ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
push _ ∈ _ at hx hy
      obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
      all_goals simp_all [mul_mem]

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:
constructor <;>
    · rintro ⟨x, x_in, hx⟩
      exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩

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

Goal state before:
pp: G₁ : Type u_7
G₂ : Type u_8
inst✝¹ : Group G₁
inst✝ : Group G₂
K : Subgroup G₂
f : G₁ →* G₂
h : f.range ≤ K
⊢ f.range.subgroupOf K = (f.codRestrict K ⋯).range

Tactic:
ext k
  refine exists_congr ?_
  simp [Subtype.ext_iff]

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 * x⁻¹) = 1

Tactic:
mul_inv_cancel,

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
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 1 = 1
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ f (y * y⁻¹) = 1

Tactic:
mul_inv_cancel,

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ f 1 = 1
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ (bit b n).bits = b :: n.bits

Tactic:
by
  rw [Nat.bits, Nat.bits, binaryRec_eq]
  simpa

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

Goal state before:
pp: A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x) = ↑(Subgroup.zpowers (Multiplicative.ofAdd x))

Tactic:
symm
  rw [Equiv.eq_image_iff_symm_image_eq]
  exact ofMul_image_zpowers_eq_zmultiples_ofMul

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : ⇑(MulAut.conj g) '' s = s
⊢ g ∈ normalizer ↑(closure s)

Tactic:
rw [mem_normalizer_iff_map_conj_eq, MonoidHom.map_closure, MonoidHom.coe_coe, hg]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
⊢ H ≤ normalizer s ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ s

Tactic:
by
  refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩
  simpa [mul_assoc] using hH h⁻¹ (inv_mem hh) _ hk

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ≤ normalizer ↑K ↔ ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K

Tactic:
by
  refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩
  simpa [mul_assoc] using hH h⁻¹ (inv_mem hh) _ hk

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
s t : Set α
⊢ op '' s • t = t * s

Tactic:
rw [← image2_smul, ← image2_mul, image2_image_left, image2_swap]
  rfl

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ {a} * s ∪ {b} * s = a • s ∪ b • s

Tactic:
singleton_mul,

Goal state after:
α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ (fun x ↦ a * x) '' s ∪ {b} * s = a • s ∪ b • s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A' A B : Subgroup G
hN : (A'.subgroupOf A).Normal
⊢ ((A' ⊓ B).subgroupOf (A ⊓ B)).Normal

Tactic:
by
  rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢
  rw [inf_inf_inf_comm, inf_idem]
  exact le_trans (inf_le_inf hN B.le_normalizer) inf_normalizer_le_normalizer_inf

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * (a * (b * b⁻¹)) ∈ H
⊢ b * a ∈ H

Tactic:
mul_inv_cancel,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * (a * 1) ∈ H
⊢ b * a ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ = 1

Tactic:
apply hdis.le_bot

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ H₁ ⊓ H₂