mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  replace hn : 0 < (n : k) := by norm_cast
  have : ∀ {l : ℤ}, 0 ≤ l → fract ((l : k) / n) = ↑(l % n) / n := by
    intro l hl
    obtain ⟨l₀, rfl | rfl⟩ := l.eq_nat_or_neg
    · rw [cast_natCast, ← natCast_mod, cast_natCast, fract_div_natCast_eq_div_natCast_mod]
    · rw [Right.nonneg_neg_iff, natCast_nonpos_iff] at hl
      simp [hl]
  obtain ⟨m₀, rfl | rfl⟩ := m.eq_nat_or_neg
  · exact this (natCast_nonneg m₀)
  let q := ⌈↑m₀ / (n : k)⌉
  let m₁ := q * ↑n - (↑m₀ : ℤ)
  have hm₁ : 0 ≤ m₁ := by
    simpa [m₁, ← @cast_le k, ← div_le_iff₀ hn] using FloorRing.gc_ceil_coe.le_u_l _
  calc
    fract ((Int.cast (-(m₀ : ℤ)) : k) / (n : k))
      = fract (-(m₀ : k) / n) := by simp
    _ = fract ((m₁ : k) / n) := ?_
    _ = Int.cast (m₁ % (n : ℤ)) / Nat.cast n := this hm₁
    _ = Int.cast (-(↑m₀ : ℤ) % ↑n) / Nat.cast n := ?_
  · rw [← fract_intCast_add q, ← mul_div_cancel_right₀ (q : k) hn.ne', ← add_div, ← sub_eq_add_neg]
    simp [m₁]
  · congr 2
    simp only [m₁]
    rw [sub_eq_add_neg, add_comm (q * ↑n), add_mul_emod_self_right]

Goal state after:
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
m : ℤ
hm : y ^ m ≤ x
⊢ m ≤ ↑M

Tactic:
contrapose! 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 : ℕ
m : ℤ
hm : y ^ m ≤ x
hM : ↑M < m
⊢ y ^ M ≤ x
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ |1 * δ| ≤ δ

Tactic:
one_mul,

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ |δ| ≤ δ
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₃ /ₛ p₂) * (p₁ /ₛ p₃) = p₁ /ₛ p₂

Tactic:
mul_comm,

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₃) * (p₃ /ₛ p₂) = p₁ /ₛ p₂
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ countP (r x) (y ::ₘ s) = countP (r x) (b ::ₘ bs)

Tactic:
countP_cons,

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (countP (r x) s + if r x y then 1 else 0) = countP (r x) (b ::ₘ bs)
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (countP (r x) s + if r x y then 1 else 0) = countP (r x) (b ::ₘ bs)

Tactic:
countP_cons,

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (countP (r x) s + if r x y then 1 else 0) = countP (r x) bs + if r x b then 1 else 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a b : α
⊢ b ∈ {a} ↔ b = a

Tactic:
simp only [← cons_zero, mem_cons, iff_self, or_false, notMem_zero]

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

Goal state before:
pp: case mpr
α : Type u_1
s t : Multiset α
⊢ s = t → Rel (fun x1 x2 ↦ x1 = x2) s t

Tactic:
rintro rfl
    exact rel_eq_refl

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

Goal state before:
pp: α : Type u
β : Type v
r : α → β → Prop
hr : Relator.BiUnique r
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
hab : r a✝ b✝
h : Forall₂ r l₁✝ l₂✝
⊢ (fun x1 x2 ↦ x1 ↔ x2) (a✝ :: l₁✝).Nodup (b✝ :: l₂✝).Nodup

Tactic:
by
    simpa only [nodup_cons] using
      Relator.rel_and (Relator.rel_not (rel_mem hr hab h)) (rel_nodup hr h)

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ s.card.pred = if a ∈ s then s.card.pred else s.card

Tactic:
if_pos

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ s.card.pred = s.card.pred

case pos.hc
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ a ∈ s
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
hstu : s + t = u
⊢ s = s + t - t

Tactic:
Multiset.add_sub_cancel_right

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
hstu : s + t = u
⊢ s = s
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ foldl erase ↑l₁ ↑l₂ = ↑(List.foldl List.erase l₁ l₂)

Tactic:
exact foldl_hom _ fun x y => rfl

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

Goal state before:

Tactic:
x = z := z_unique x px
        _ = y := (z_unique y py).symm

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s + u - u - t = s - t

Tactic:
Multiset.add_sub_cancel_right

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s - t = s - t
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case mpr
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ n < (filter P s).card → ∃ s', s' ≤ s ∧ n < s'.card ∧ ∀ (a : α), a ∈ s' → P a

Tactic:
exact fun H ↦ ⟨s.filter P, filter_le _ _, H, fun a ha ↦ (mem_filter.mp ha).2⟩

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

Goal state before:
pp: case none
α : Type u_1
β : Type v
f : α → Option β
a : α
s : Multiset α
h : f a = none
⊢ filterMap f (a ::ₘ s) = (Option.map singleton none).getD 0 + filterMap f s

Tactic:
| none =>

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ countP p (f a ::ₘ map f t) = (filter (fun a ↦ p (f a)) (a ::ₘ t)).card

Tactic:
countP_cons,

Goal state after:
case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ (countP p (map f t) + if p (f a) then 1 else 0) = (filter (fun a ↦ p (f a)) (a ::ₘ t)).card
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) i
hj : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
⊢ x ∈ t ∧ f x = i

Tactic:
simpa using hi hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Set α
⊢ ↑s.toFinset = s

Tactic:
classical exact s.coe_toFinset

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

Goal state before:
pp: n m : ℕ
hmn : n ≤ m
⊢ Set.range ⇑(natAdd_castLEEmb hmn) = {i | m - n ≤ ↑i}

Tactic:
by
  simp only [natAdd_castLEEmb, Nat.sub_le_iff_le_add]
  ext y
  exact ⟨fun ⟨x, hx⟩ ↦ by simp [← hx]; lia,
    fun xin ↦ ⟨subNat (m - n) (y.cast (Nat.add_sub_of_le hmn).symm)
    (Nat.sub_le_of_le_add xin), by simp⟩⟩

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

Goal state before:
pp: case calc_2.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
h : b ∈ t
⊢ b ∈ image (fun a ↦ i ↑a ⋯) s.attach

Tactic:
obtain ⟨a, ha, rfl⟩ := i_surj b h; exact mem_image.2 ⟨⟨a, ha⟩, by simp⟩

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

Goal state before:
pp: case mpr
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ (∀ (i : Fin n), r (f i.castSucc) (f i.succ)) → ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f

Tactic:
refine fun H i => Fin.induction (fun h ↦ ?_) ?_

Goal state after:
case mpr.refine_1
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
h : (fun x1 x2 ↦ x1 < x2) i 0
⊢ r (f i) (f 0)

case mpr.refine_2
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
⊢ ∀ (i_1 : Fin n),
    ((fun x1 x2 ↦ x1 < x2) i i_1.castSucc → r (f i) (f i_1.castSucc)) →
      (fun x1 x2 ↦ x1 < x2) i i_1.succ → r (f i) (f i_1.succ)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hi : i ≠ last n
hj : j ≠ last n
⊢ ↑(i.castPred hi) ≤ ↑(j.castPred hj) ∧ ↑(j.castPred hj) ≤ ↑(i.castPred hi) ↔ ↑i ≤ ↑j ∧ ↑j ≤ ↑i

Tactic:
← le_def,

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hb : b ≠ 0
⊢ (a.castPred ha).succ ≤ b ↔ a < b

Tactic:
succ_castPred_le_iff

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hb : b ≠ 0
⊢ a < b ↔ a < b
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i = 0
⊢ predAbove 0 i = 0

Tactic:
rw [hi, predAbove_right_zero]

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

Goal state before:
pp: case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ g (cons y q j'.succ) = g (q j')

Tactic:
cons_succ

Goal state after:
case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ g (q j') = g (q j')
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ (∃ a b c, a ∈ univ ∧ b ∈ univ ∧ c ∈ univ ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
mem_univ,

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ (∃ a b c, True ∧ True ∧ True ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ append x₀ x (castAdd n i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n i)

Tactic:
rw [Subsingleton.elim i 0, Fin.append_left, Function.comp_apply, eq_comm]

Goal state after:
case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ cons (x₀ 0) x (Fin.cast ⋯ (castAdd n 0)) = x₀ 0
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:
cons_succ

Goal state after:
case succ.cast
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
j : Fin n
⊢ snoc q b j.castSucc = snoc (cons a q) b j.castSucc.succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ ∀ (i : Fin n), append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)

Tactic:
intro i
    rw [Fin.append_left]
    exact (@snoc_castSucc _ (fun _ => α) _ _ i).symm

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

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

Tactic:
← union_compl_self s

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedGE ↔ l.SortedGE

Tactic:
← sortedLE_reverse,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).reverse.SortedLE ↔ l.reverse.SortedLE
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ Fin.find p h ∈ find? fun b ↦ decide (p b)

Tactic:
by grind [find?_eq_dite]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
m : Multiset ι
⊢ (map (fun x ↦ 1) m).prod = 1

Tactic:
by
  rw [map_const', prod_replicate, one_pow]

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l₁ l₂ : List G
⊢ a / (l₁.alternatingProd * l₂.alternatingProd ^ (-1) ^ l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-(1 * (-1) ^ l₁.length))

Tactic:
one_mul,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l₁ l₂ : List G
⊢ a / (l₁.alternatingProd * l₂.alternatingProd ^ (-1) ^ l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-(-1) ^ l₁.length)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ l.alternatingProd ^ (-(1 * (-1) ^ l.length)) * a ^ (-1) ^ l.length =
    (a / l.alternatingProd) ^ (-(1 * -(1 * (-1) ^ l.length)))

Tactic:
one_mul,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ l.alternatingProd ^ (-(-1) ^ l.length) * a ^ (-1) ^ l.length = (a / l.alternatingProd) ^ (- -(-1) ^ l.length)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ (l.alternatingProd ^ (-1) ^ l.length)⁻¹ * a ^ (-1) ^ l.length = (a / l.alternatingProd) ^ (-1) ^ l.length

Tactic:
mul_comm,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ a ^ (-1) ^ l.length * (l.alternatingProd ^ (-1) ^ l.length)⁻¹ = (a / l.alternatingProd) ^ (-1) ^ l.length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
· rw [mod_eq_of_lt (Nat.sub_lt hl hn), Nat.sub_add_cancel, mod_self, rotate_zero]
      exact (Nat.mod_lt _ hl).le

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

Goal state before:
pp: α : Type u_1
a : α
S : Multiset (Multiset α)
⊢ ∀ (a_1 : Multiset α) (s : Multiset (Multiset α)),
    (a ∈ s.join ↔ ∃ s_1, s_1 ∈ s ∧ a ∈ s_1) → (a ∈ (a_1 ::ₘ s).join ↔ ∃ s_1, s_1 ∈ a_1 ::ₘ s ∧ a ∈ s_1)

Tactic:
simp +contextual [or_and_right, exists_or]

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
⊢ (s.bind fun x ↦ 0) = 0

Tactic:
by simp [bind, join, nsmul_zero]

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

Goal state before:
pp: case none
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
ham : a ∈ m
⊢ ((Option.map singleton none).getD 0).bind g = (Option.map g none).getD 0

Tactic:
| none =>

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

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

Tactic:
by
  simp only [filterMap_eq_bind, Multiset.bind_assoc]
  apply Multiset.bind_congr; intro a ham
  cases f a with
  | none => simp
  | some b => simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
G : Type u_4
inst✝ : DivisionCommMonoid G
m : Multiset ι
f : ι → G
n : ℤ
⊢ (map (fun i ↦ f i ^ n) m).prod = (map f m).prod ^ n

Tactic:
convert! (m.map f).prod_hom (zpowGroupHom n : G →* G)

Goal state after:
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)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
⊢ l.cyclicPermutations.head? = some l

Tactic:
rw [head?_eq_some_head (cyclicPermutations_ne_nil l), head_cyclicPermutations]

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

Goal state before:
pp: α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ (l.rotate k).cyclicPermutations.get ⟨n, hn⟩ = (l.cyclicPermutations.rotate k).get ⟨n, hn'⟩

Tactic:
get_rotate,

Goal state after:
α : Type u
l : List α
k : ℕ
this : (l.rotate k).cyclicPermutations.length = (l.cyclicPermutations.rotate k).length
n : ℕ
hn : n < (l.rotate k).cyclicPermutations.length
hn' : n < (l.cyclicPermutations.rotate k).length
⊢ (l.rotate k).cyclicPermutations.get ⟨n, hn⟩ =
    l.cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % l.cyclicPermutations.length, ⋯⟩
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
f : α → β
s✝ : Finset α
t : β → Finset γ
this : DecidableEq α
a : α
s : Finset α
x✝ : a ∉ s
ih : (image f s).biUnion t = s.biUnion fun a ↦ t (f a)
⊢ (image f (insert a s)).biUnion t = (insert a s).biUnion fun a ↦ t (f a)

Tactic:
by simp only [image_insert, biUnion_insert, ih]

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

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

Tactic:
rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, add_one_mul_choose_eq]

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

Goal state before:
pp: case inr
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
h : Nonempty (α ↪ β)
f : α ↪ β
this : Finite α
⊢ Finite (α ↪ β)

Tactic:
exact Finite.of_injective _ DFunLike.coe_injective

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : ↑c * a = b * ↑c
⊢ a = b

Tactic:
mul_comm,

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : a * ↑c = b * ↑c
⊢ a = b
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
p : M → Prop
s : Set M
closure : Subsemigroup.closure s = ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
x✝ : x ∈ Subsemigroup.closure s
⊢ p x

Tactic:
induction closure.symm ▸ mem_top x using closure_induction with

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
motive : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
x✝ : x ∈ Submonoid.closure s
⊢ motive x

Tactic:
induction closure.symm ▸ mem_top x using closure_induction with

Goal state after:
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.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x y : M
⊢ f (1 * y) = f 1 * f y

Tactic:
one_mul,

Goal state after:
M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x y : M
⊢ f y = f 1 * f y
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ map K.subtype (H.subgroupOf K) = H

Tactic:
subgroupOf_map_subtype,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ H ⊓ K = H
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:
by
  ext k
  refine exists_congr ?_
  simp [Subtype.ext_iff]

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

Goal state before:
pp: case mp.refine_3
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x y : G),
    x ∈ closure (↑s ∪ ↑t) →
      y ∈ closure (↑s ∪ ↑t) →
        (∃ y ∈ s, ∃ z ∈ t, y * z = x) → (∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y) → ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = x * y

pp: case mp.refine_4
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ closure (↑s ∪ ↑t), (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹

Tactic:
· rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
      exact ⟨y₁ * y₂, s.mul_mem hy₁ hy₂,
            (y₂⁻¹ * z₁ * y₂) * z₂, t.mul_mem (ht.conj_mem' z₁ hz₁ y₂) hz₂, by simp [mul_assoc]⟩

Goal state after:
case mp.refine_4
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ closure (↑s ∪ ↑t), (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mp
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ s.prod t ≤ u → map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u

Tactic:
intro h
    constructor
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨hx, Submonoid.one_mem _⟩
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨Submonoid.one_mem _, hx⟩

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

Goal state before:
pp: case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u → s.prod t ≤ u

Tactic:
rintro ⟨hH, hK⟩ ⟨x1, x2⟩ ⟨h1, h2⟩

Goal state after:
case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
⊢ (x1, x2) ∈ u
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mrange (inl M N) ⊔ mrange (inr M N) = ⊤

Tactic:
simp only [mrange_inl, mrange_inr, prod_bot_sup_bot_prod, top_prod_top]

Goal state after: