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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ -1 - 1 ≤ a - 1

Tactic:
sub_le_sub_iff_right

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ -1 ≤ a
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
s : Set R
⊢ fract ⁻¹' s = ⋃ m, (fun x ↦ x - ↑m) ⁻¹' (s ∩ Ico 0 1)

Tactic:
ext x
  simp only [mem_preimage, mem_iUnion, mem_inter_iff]
  refine ⟨fun h => ⟨⌊x⌋, h, fract_nonneg x, fract_lt_one x⟩, ?_⟩
  rintro ⟨m, hms, hm0, hm1⟩
  obtain rfl : ⌊x⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩
  exact hms

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
⊢ ⌈q⌉ = -(-q.num / ↑q.den)

Tactic:
change -⌊-q⌋ = _
  rw [Rat.floor_def', num_neg_eq_neg_num, den_neg_eq_den]

Goal state after:
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✝² : AddCommGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℤ
x : G
⊢ f (n • a + x) = f x + n • b

Tactic:
by
  rw [add_comm, map_add_zsmul]

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
⊢ 0 < (1 - fract q) * ↑q.den

Tactic:
have : 0 < 1 - fract q := by
    have : fract q < 1 := fract_lt_one q
    have : 0 + fract q < 1 := by simp [this]
    rwa [lt_sub_iff_add_lt]

Goal state after:
q : ℚ
this : 0 < 1 - fract q
⊢ 0 < (1 - fract q) * ↑q.den
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : (↑q.den).natAbs.Coprime q.num.natAbs
this✝ : (↑q.den).natAbs = q.den
this : ↑(↑q.den / ↑q.num).den = ↑q.num.natAbs
⊢ (↑q.den / ↑q.num).den = q.num.natAbs

Tactic:
exact mod_cast this

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a b : R
⊢ Int.cast ⁻¹' Ioo a b = Ioo ⌊a⌋ ⌈b⌉

Tactic:
ext
  simp [floor_lt, lt_ceil]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : -1 < a
⊢ ↑⌈a⌉₊ = ⌈a⌉

Tactic:
rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg_of_neg_one_lt ha)]

Goal state after:
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
M : Type u_6
N : Type u_7
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MulDistribMulAction M N
m : M
u : Nˣ
⊢ m • ↑u * m • ↑u⁻¹ = 1

Tactic:
by simp [← smul_mul', smul_one]

Goal state after:
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
M : Type u_6
N : Type u_7
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MulDistribMulAction M N
m : M
u : Nˣ
⊢ m • ↑u⁻¹ * m • ↑u = 1

Tactic:
by simp [← smul_mul', smul_one]

Goal state after:
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
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
⊢ ∃ z, x < ↑z / ↑n ∧ ↑z / ↑n < y

Tactic:
obtain ⟨z, zh⟩ := exists_floor (x * n)
  refine ⟨z + 1, ?_⟩
  have n0' := (inv_pos.2 (sub_pos.2 h)).trans nh
  rw [div_lt_iff₀ n0']
  refine ⟨(lt_div_iff₀ n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), ?_⟩
  rw [Int.cast_add, Int.cast_one]
  grw [(zh _).1 le_rfl]
  rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff₀' (sub_pos.2 h), one_div]

Goal state after:
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
⊢ (↑m * δ) ^ n - (y - max x 0) < (↑m * δ) ^ n - ((↑m * δ) ^ n - q ^ n)

Tactic:
refine sub_lt_sub_left ((le_abs_self _).trans_lt <| cont _ _ q1y.le ?_) _

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
⊢ |↑m * δ - q| ≤ δ
Module: Mathlib.Algebra.Torsor.Basic

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

Tactic:
mul_div_assoc,

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

Goal state before:
pp: α : Type u_1
a b : α
m : Multiset α
⊢ {a} = b ::ₘ m ↔ a = b ∧ m = 0

Tactic:
← cons_zero,

Goal state after:
α : Type u_1
a b : α
m : Multiset α
⊢ a ::ₘ 0 = b ::ₘ m ↔ a = b ∧ m = 0
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
⊢ l.dedup = a :: l' ↔ a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
  · refine ⟨mem_dedup.1 (h.symm ▸ mem_cons_self), fun ha => ?_, by rw [h, tail_cons]⟩
    have := count_pos_iff.2 ha
    have : count a l.dedup ≤ 1 := nodup_iff_count_le_one.1 (nodup_dedup l) a
    rw [h, count_cons_self] at this
    lia
  · have := @List.cons_head!_tail α ⟨a⟩ _ (ne_nil_of_mem (mem_dedup.2 h.1))
    have hal : a ∈ l.dedup := mem_dedup.2 h.1
    rw [← this, mem_cons, or_iff_not_imp_right] at hal
    exact this ▸ h.2.2.symm ▸ cons_eq_cons.2 ⟨(hal (h.2.2.symm ▸ h.2.1)).symm, rfl⟩

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
⊢ countP p (filter q s) = countP (fun a ↦ p a ∧ q a) s

Tactic:
by simp [countP_eq_card_filter]

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

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

Tactic:
simp [inits_eq_tails l, map_inj_left, ← map_reverse]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ ↑s ⊆ ↑t ↔ s ⊆ t

pp: α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ a ∉ ↑s

Tactic:
coe_subset

Goal state after:
α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ s ⊆ t ↔ s ⊆ t

α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ a ∉ ↑s
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ {a}.toFinset = {a}

Tactic:
← cons_zero,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ (a ::ₘ 0).toFinset = {a}
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:
by simpa using hi hx

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

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

Tactic:
obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = j := by simpa using hj hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t u : Finset α
x : α
hx : x ∈ u
hi hj : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) (f x)
h : f x ≠ f x
⊢ x ∈ ⊥
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
n : ℕ
ih : (image f)^[n] s = image f^[n] s
⊢ (image f)^[n + 1] s = image f^[n + 1] s

Tactic:
iterate_succ_apply',

Goal state after:
case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
n : ℕ
ih : (image f)^[n] s = image f^[n] s
⊢ image f ((image f)^[n] s) = image f^[n + 1] s
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ℕ
⊢ a % m = a % m % n

Tactic:
rw [Nat.mod_eq_of_lt (a := a % m) (lt_of_lt_of_le (Nat.mod_lt _ m.pos_of_neZero) h)]

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc < p ∨ p < i.succ

Tactic:
simp [Fin.lt_def, -val_fin_lt]

Goal state after:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ ↑i < ↑p ∨ ↑p < ↑i + 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
i j : Fin (n + 1)
h : i ≤ j
hj : j ≠ last n
⊢ i ≠ last n

Tactic:
rw [← lt_last_iff_ne_last] at hj ⊢

Goal state after:
n m : ℕ
i j : Fin (n + 1)
h : i ≤ j
hj : j < last n
⊢ i < last n
Module: Mathlib.Data.Finset.Card

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

Tactic:
sdiff_union_inter

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #s = #s
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
⊢ (∃ x, s ⊆ {x}) → #s ≤ 1

Tactic:
· rintro ⟨x, hx⟩
    rw [← card_singleton x]
    exact card_le_card hx

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
h : x ∈+ x :: l
⊢ x ∈ l

Tactic:
obtain h | h := h
  · exact h
  · exact h.mem

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

Goal state before:
pp: n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
⊢ append (snoc xs x) ys = append xs (cons x ys) ∘ Fin.cast ⋯

Tactic:
by
  rw [snoc_eq_append, append_assoc, append_left_eq_cons, append_cast_right]; rfl

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

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ tl[ix]? = (hd :: tl)[ix + 1]?

Tactic:
simp only [getElem?_cons_succ]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
x : α
_hx : x ∉ ∅
y : α
hy : y ∉ {x}
⊢ y ≠ x

Tactic:
simpa only [mem_singleton] using hy

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

Goal state before:
pp: case cons.hl₂
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r x a ↔ s (f x) (f a))

Tactic:
simpa only [mem_insertionSort] using hl.1.2

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
s : Set α
hs : sᶜ.Finite
h : s.Finite
⊢ univ.Finite

Tactic:
simpa using hs.union h

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
s : Set α
hs : s.Finite
h : sᶜ.Finite
⊢ univ.Finite

Tactic:
simpa using hs.union h

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

Goal state before:
pp: m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin (m + n)
hi : i < natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)
⊢ ¬p i

Tactic:
cases i using addCases with

Goal state after:
case left
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin m
hi : castAdd n i < natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)
⊢ ¬p (castAdd n i)

case right
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin n
hi : natAdd m i < natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)
⊢ ¬p (natAdd m i)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin (m + n)
hi : i < natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)
⊢ ¬p i

Tactic:
cases i using addCases with | left i => _ | right i => _

Goal state after:
case left
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin m
hi : castAdd n i < natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)
⊢ ¬p (castAdd n i)

case right
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin n
hi : natAdd m i < natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)
⊢ ¬p (natAdd m i)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ ((r c b ∧ r c (f a)) ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)

Tactic:
and_assoc

Goal state after:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ (r c b ∧ r c (f a) ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)
Module: Mathlib.Data.List.Range

Goal state before:
pp: case cons
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (a :: l).ranges

Tactic:
simp only [ranges, pairwise_cons]

Goal state after:
case cons
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ (∀ (a' : List ℕ), a' ∈ map (map fun x ↦ a + x) l.ranges → (range a).Disjoint a') ∧
    Pairwise Disjoint (map (map fun x ↦ a + x) l.ranges)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ (R a b ∧ IsChain R (b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    (R a b ∧ IsChain R (b :: l₁)) ∧
      IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y

Tactic:
and_assoc

Goal state after:
α : Type u_1
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ (R a b ∧ IsChain R (b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    R a b ∧
      IsChain R (b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: l : List ℤ
h : l.prod = -1
⊢ -1 ∈ l

Tactic:
obtain ⟨x, h₁, h₂⟩ := exists_mem_ne_one_of_prod_ne_one (ne_of_eq_of_ne h (by decide))
  exact Or.resolve_left
    (Int.isUnit_iff.mp (prod_isUnit_iff.mp
      (h.symm ▸ ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩ : IsUnit l.prod) x h₁)) h₂ ▸ h₁

Goal state after:
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:
simp [isChain_eq_iff_eq_replicate, replicate_succ]

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
n : ℕ
h : s.Nodup
hn : n ≠ 0
⊢ s ≤ n • t ↔ s ≤ t

Tactic:
simp [← h.le_dedup_iff_le, hn]

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

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

Tactic:
simp [getElem_rotate]

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

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

Tactic:
by
  rw [getElem_rotate]
  refine congr_arg l.get (Fin.eq_of_val_eq ?_)
  simp only [mod_add_mod]
  rw [← add_mod_mod, Nat.add_right_comm, Nat.sub_add_cancel, add_mod_left, mod_eq_of_lt]
  exacts [hk, (mod_lt _ (k.zero_le.trans_lt hk)).le]

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

Goal state before:
pp: case cons.intro.intro.cons.cons
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝¹ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l✝ : List α
hl' : List.IsChain (flip r) l✝
l' l : List.chains r
h✝ : ∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y
ihl :
  ∀ (y : List.chains r),
    List.lex_chains r y l → ∀ (hl : List.IsChain (flip r) (a :: ↑y)), Acc (List.lex_chains r) ⟨a :: ↑y, hl⟩
hl : List.IsChain (flip r) (a :: ↑l)
m : List α
hm : List.IsChain (flip r) (a :: m)
hr : List.Lex r m ↑l
⊢ Acc (List.lex_chains r) ⟨a :: m, hm⟩

Tactic:
· apply ihl ⟨m, (List.isChain_cons.1 hm).2⟩ hr

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

Goal state before:
pp: α : Type u_1
L✝ : List α
a b : α
L : List α
hL : a :: b :: L ≠ []
hL' : (a :: b :: L).head hL = (a :: b :: L).getLast hL
⊢ (a :: b :: L).dropLast ~r (a :: b :: L).tail

Tactic:
simp only [head_cons, ne_eq, reduceCtorEq, not_false_eq_true, getLast_cons] at hL'
    simp [hL', IsRotated.cons_getLast_dropLast]

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

Goal state before:
pp: α : Type u_1
L✝ : List α
a b : α
L : List α
hL : a :: b :: L ≠ []
hL' : (a :: b :: L).head hL = (a :: b :: L).getLast hL
⊢ (a :: b :: L).dropLast ~r (a :: b :: L).tail

Tactic:
by
    simp only [head_cons, ne_eq, reduceCtorEq, not_false_eq_true, getLast_cons] at hL'
    simp [hL', IsRotated.cons_getLast_dropLast]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.offDiag.length = l.length * (l.length - 1)

Tactic:
have : ∀ x ∈ l.zipIdx, length (eraseIdx l x.2) = length l - 1 := fun x hx ↦
    length_eraseIdx_of_lt <| snd_lt_of_mem_zipIdx hx
  simp [offDiag, map_congr_left this]

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

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

Tactic:
rw [choose_succ_right _ _ hn, Nat.add_one_sub_one]

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

Goal state before:
pp: case inr
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)

Tactic:
have h : 0 < (n - k)! * (k - s)! * s ! := by apply_rules [factorial_pos, Nat.mul_pos]

Goal state after:
case inr
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
h : 0 < (n - k)! * (k - s)! * s !
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SMul α β
a : α
S : Set (Set β)
⊢ a • ⋃₀ S = ⋃ s ∈ S, a • s

Tactic:
sUnion_eq_biUnion,

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : SMul α β
a : α
S : Set (Set β)
⊢ a • ⋃ i ∈ S, i = ⋃ s ∈ S, a • s
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
⊢ f ⁻¹' ⋃₀ s = ⋃ t ∈ s, f ⁻¹' t

Tactic:
sUnion_eq_biUnion,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
⊢ f ⁻¹' ⋃ i ∈ s, i = ⋃ t ∈ s, f ⁻¹' t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
C : Set (Set β)
⊢ s ×ˢ ⋃₀ C = ⋃₀ ((fun t ↦ s ×ˢ t) '' C)

Tactic:
sUnion_eq_biUnion,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
C : Set (Set β)
⊢ s ×ˢ ⋃ i ∈ C, i = ⋃ i ∈ (fun t ↦ s ×ˢ t) '' C, i
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : ∀ (h : G), h * g ∈ S ↔ g * h ∈ S
n : G
⊢ n ∈ S ↔ n * g⁻¹ * g ∈ S

Tactic:
inv_mul_cancel_right

Goal state after:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : ∀ (h : G), h * g ∈ S ↔ g * h ∈ S
n : G
⊢ n ∈ S ↔ n ∈ S
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 1

Tactic:
Subtype.nontrivial_iff_exists_ne (fun x => x ∈ H) (1 : H)

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ y, ∃ (_ : y ∈ H), y ≠ ↑1) ↔ ∃ x ∈ H, x ≠ 1
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:
hx,

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 x⁻¹ = 1 * f x⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_1
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ ↑s ∪ ↑t, ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
rintro y (h | h)

Goal state after:
case refine_1.inl
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑s
⊢ ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y

case refine_1.inr
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑t
⊢ ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y
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

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:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
S : Submonoid M
f : M →* N
⊢ mrange (f.domRestrict S) = map f S

Tactic:
by
  simp [SetLike.ext_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ zpowers g ≤ ⊥ ↔ g = 1

Tactic:
zpowers_le,

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
⊢ g ∈ ⊥ ↔ g = 1
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A : Set β
a : α
x : β
⊢ x ∈ a⁻¹ • A ↔ a • x ∈ A

Tactic:
simp only [← image_smul, mem_image, inv_smul_eq_iff, exists_eq_right]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
a : α
⊢ s = a⁻¹ • univ ↔ s = univ

Tactic:
smul_set_univ

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
a : α
⊢ s = univ ↔ s = univ