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

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = ↑⌊a⌋ + 1

Tactic:
← Int.cast_one,

Goal state after:
case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = ↑⌊a⌋ + ↑1
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
this : ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
⊢ ((↑q.den - ↑q.num * ↑⌊↑q.den / ↑q.num⌋) / ↑q.num).num < q.num

Tactic:
simp [q_inv, this]

Goal state after:
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
this : q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + 1 * ↑q⁻¹.den
⊢ q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den

Tactic:
one_mul

Goal state after:
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
this : q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den
⊢ q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den
Module: Mathlib.Algebra.Torsor.Defs

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:
rw [← one_mul (p /ₛ p), ← smul_sdiv_assoc, smul_sdiv]

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

Goal state before:
pp: G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : B →* A
hf : Injective ⇑f
smul : ∀ (c : M) (x : B), f (c • x) = c • f x
c : M
⊢ f (c • 1) = f 1

Tactic:
by simp only [smul, f.map_one, 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
h : x < y
⊢ ∃ q, x < ↑q ∧ ↑q < y

Tactic:
by
  obtain ⟨n, nh⟩ := exists_nat_gt (y - x)⁻¹
  obtain ⟨z, zh, zh'⟩ := exists_div_btwn h nh
  refine ⟨(z : ℚ) / n, ?_, ?_⟩ <;> simpa

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
⊢ count a {b} = if a = b then 1 else 0

Tactic:
by
  simp only [count_cons, ← cons_zero, count_zero, Nat.zero_add]

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

Goal state before:
pp: α : Type u
β : Type v
l₁ : List α
f : α → List β
⊢ (flatMap f l₁).Nodup ↔ (∀ (x : α), x ∈ l₁ → (f x).Nodup) ∧ Pairwise (Disjoint on f) l₁

Tactic:
by
  simp only [List.flatMap, nodup_flatten, pairwise_map, and_comm, mem_map,
    exists_imp, and_imp]
  rw [show (∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔ ∀ x : α, x ∈ l₁ → Nodup (f x)
      from forall_comm.trans <| forall_congr' fun _ => forall_eq']

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
p : l₁ ~ l₂
a : α
h : a ∈ l₁
⊢ List.count a l₁.dedup = List.count a l₂.dedup

Tactic:
by
      simp [h, nodup_dedup, p.subset h]

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

Goal state before:
pp: case refine_2
α : Type u_1
s t : Multiset α
h : ∀ {a : α}, a ∈ s → ¬a ∈ t
u : Multiset α
hs : u ≤ s
ht : u ≤ t
⊢ u ≤ ⊥

Tactic:
· rw [le_bot_iff, bot_eq_zero, eq_zero_iff_forall_notMem]
    exact fun a ha ↦ h (subset_of_le hs ha) (subset_of_le ht ha)

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.drop n l₁ <+: List.drop n l₂

Tactic:
rw [prefix_iff_eq_take.mp h, drop_take]

Goal state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.take (l₁.length - n) (List.drop n l₂) <+: List.drop n l₂
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <+: l₂
⊢ l₁.flatten <+: l₂.flatten

Tactic:
by
  rcases h with ⟨l, rfl⟩
  simp

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <:+ l₂
⊢ l₁.flatten <:+ l₂.flatten

Tactic:
by
  rcases h with ⟨l, rfl⟩
  simp

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

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

Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty

Goal state after:
case cons.inl
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
ha : a ∉ ∅
h : ∀ (hs : ∅.Nonempty), motive ∅ hs
hs : (Finset.cons a ∅ ha).Nonempty
⊢ motive (Finset.cons a ∅ ha) hs

case cons.inr
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
t : Finset α
ha : a ∉ t
h : ∀ (hs : t.Nonempty), motive t hs
hs : (Finset.cons a t ha).Nonempty
ht : t.Nonempty
⊢ motive (Finset.cons a t ha) hs
Module: Mathlib.Data.Finset.Range

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ (range n).Nontrivial

Tactic:
Finset.Nontrivial,

Goal state after:
n : ℕ
hn : 1 < n
⊢ (↑(range n)).Nontrivial
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ univ.Nontrivial ↔ Nontrivial α

Tactic:
Finset.Nontrivial,

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ (↑univ).Nontrivial ↔ Nontrivial α
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset.Nontrivial ↔ s.Nontrivial

Tactic:
Finset.Nontrivial,

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ (↑s.toFinset).Nontrivial ↔ s.Nontrivial
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 0 = ⊤ ↔ n = 1

Tactic:
rw [← bot_eq_zero, subsingleton_iff_bot_eq_top, subsingleton_iff_le_one,
    le_one_iff_eq_zero_or_eq_one, or_iff_right (NeZero.ne n)]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
⊢ 0 < p.succAbove i

Tactic:
by_cases H : castSucc i < p

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : i.castSucc < p
⊢ 0 < p.succAbove i

case neg
n : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : ¬i.castSucc < p
⊢ 0 < p.succAbove i
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (ofFn (Fin.cons x₀ xs)).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs

Tactic:
simp_rw [ofFn_succ, Fin.cons_succ, nodup_cons, Fin.cons_zero, mem_ofFn] at h

Goal state after:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (¬∃ i, xs i = x₀) ∧ (ofFn fun i ↦ xs i).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ Subsingleton ↥s ↔ Subsingleton ↑↑s

Tactic:
SetLike.coe_sort_coe

Goal state after:
α : Type u_1
s : Finset α
⊢ Subsingleton ↥s ↔ Subsingleton ↥s
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ¬s.Nontrivial

Tactic:
Finset.Nontrivial,

Goal state after:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ¬(↑s).Nontrivial
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ (∀ ⦃x_1 : α⦄, x_1 ∈ {z | r z x} → x_1 ∈ {z | r z y}) ∧ ¬∀ ⦃x_1 : α⦄, x_1 ∈ {z | r z y} → x_1 ∈ {z | r z x}

Tactic:
mem_filter_univ

Goal state after:
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ (∀ ⦃x_1 : α⦄, r x_1 x → r x_1 y) ∧ ¬∀ ⦃x_1 : α⦄, r x_1 y → r x_1 x
Module: Mathlib.Data.List.Duplicate

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

Tactic:
simp [h.subset hx]

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]?
⊢ some hd = l'[f 0]?

Tactic:
simpa using hf 0

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

Goal state before:
pp: n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n.succ → α
⊢ g ∘ init q = init (g ∘ q)

Tactic:
by
  ext j
  simp [init]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
h : Fintype.card α ≤ Fintype.card β
⊢ Nonempty (α ↪ β)

Tactic:
exact (truncOfCardLE h).nonempty

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

Goal state before:
pp: n : ℕ
P : Fin (n + 1) → Prop
⊢ (∃ i, P i) → P (last n) ∨ ∃ i, P i.castSucc

Tactic:
rintro ⟨i, hi⟩
    cases i using lastCases with
    | last => exact .inl hi
    | cast _ => exact .inr ⟨_, hi⟩

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ count a (orderedInsert r b L) = count a L + if b = a then 1 else 0

Tactic:
rw [(L.perm_orderedInsert r b).count_eq, count_cons]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ (count a L + if (b == a) = true then 1 else 0) = count a L + if b = a then 1 else 0
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
h : s.Finite
⊢ h.toFinset.Nontrivial ↔ s.Nontrivial

Tactic:
Finset.Nontrivial,

Goal state after:
α : Type u
s : Set α
h : s.Finite
⊢ (↑h.toFinset).Nontrivial ↔ s.Nontrivial
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : p x
this : x ∉ filter p s
⊢ op (f x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))

Tactic:
simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]

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

Goal state before:
pp: case cons
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
⊢ p (a ::ₘ s).prod

Tactic:
rw [prod_cons]

Goal state after:
case cons
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
⊢ p (a * s.prod)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: α : Type u_2
L : List (List α)
i : ℕ
h : i < L.length
⊢ drop (take i (map length L)).sum (take (take (i + 1) (map length L)).sum L.flatten) = L[i]

Tactic:
by
  have : (L.map length).take i = ((L.take (i + 1)).map length).take i := by
    simp [map_take, take_take, Nat.min_eq_left]
  simp only [this, take_sum_flatten, drop_sum_flatten,
    drop_take_succ_eq_cons_getElem, h, flatten_nil, flatten_cons, append_nil]

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
s t : List M
h : l = s ++ a :: t
⊢ a ∣ (s ++ a :: t).prod

Tactic:
prod_append,

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
a : M
l : List M
ha : a ∈ l
s t : List M
h : l = s ++ a :: t
⊢ a ∣ s.prod * (a :: t).prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
hα : Nonempty α
a : α
l : List α
x✝ : ∃ a_1, a :: l = replicate (a :: l).length a_1
n : ℕ
b : α
hb : a :: l = replicate (a :: l).length b
⊢ (replicate (a :: l).length b).rotate n = replicate (a :: l).length b

Tactic:
rotate_replicate

Goal state after:
α : Type u
hα : Nonempty α
a : α
l : List α
x✝ : ∃ a_1, a :: l = replicate (a :: l).length a_1
n : ℕ
b : α
hb : a :: l = replicate (a :: l).length b
⊢ replicate (a :: l).length b = replicate (a :: l).length b
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
⊢ l = l'

Tactic:
← take_append_drop _ l,

Goal state after:
α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
⊢ take ?m.69 l ++ drop ?m.69 l = l'

α : Type u
n : ℕ
l l' : List α
h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'
hle : l.length = l'.length
hd : drop (n % l.length) l = drop (n % l'.length) l'
ht : take (n % l.length) l = take (n % l'.length) l'
⊢ ℕ
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons.intro.intro
α : 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)), Acc (List.lex_chains r) ⟨a :: ↑l, hl⟩

Tactic:
intro hl

Goal state after:
case cons.intro.intro
α : 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)
⊢ Acc (List.lex_chains r) ⟨a :: ↑l, hl⟩
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
hl : l.Nodup
n : ℕ
⊢ l.rotate n = l ↔ n % l.length = 0 ∨ l = []

Tactic:
rw [← zero_mod, ← hl.rotate_congr_iff, rotate_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ Function.onFun Disjoint (fun a ↦ {x ∈ s | f x = a}) x' y'

Tactic:
by
    simp_rw [disjoint_left, mem_filter]; rintro i ⟨_, rfl⟩ ⟨_, rfl⟩; exact hne rfl

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

Goal state before:
pp: case mpr
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y → ∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y

Tactic:
· rintro ⟨⟨i, hi, rfl⟩, ⟨j, hj, rfl⟩, hne⟩
    exact ⟨i, hi, j, hj, mt h.getElem_inj_iff.2 hne, rfl, rfl⟩

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

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

Tactic:
ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

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

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

Tactic:
ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset t

Tactic:
simp only [piFinset, mem_map, forall_prop_of_true, mem_univ, mem_pi]

Goal state after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → ∃ a, (∀ (a_1 : α), a a_1 ⋯ ∈ t a_1) ∧ { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } a = f
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg.hf.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ map (fun x ↦ Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' x)) n ≍ map (fun x ↦ Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b x)) n

Tactic:
apply map_hcongr

Goal state after:
case neg.hf.hf.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)

case neg.hf.hf.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ ∀ (a_1 : (a : α) → a ∈ m → β a),
    a_1 ∈ n → Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' a_1) ≍ Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b a_1)
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ t) = t

Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
a : α
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ ∅) = ∅

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
ht : t.Nonempty
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ t) = t
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
rw [← ascFactorial_eq_factorial_mul_choose]

Goal state after:
n k : ℕ
⊢ (n + 1).ascFactorial k = k ! * ((n + 1).ascFactorial k / k !)
Module: Mathlib.Algebra.Group.Action.End

Goal state before:
pp: G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
⊢ ∀ (x y : α), ∃ g, g • x = y

Tactic:
classical
  intro x y
  use Equiv.swap x y
  simp

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

Goal state before:
pp: case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ v i ⊆ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k

Tactic:
· intro y y_in
      simp only [mem_image, mem_iInter, mem_preimage]
      rcases hv with ⟨z, hz⟩
      refine ⟨Function.update z i y, ?_, update_self i y z⟩
      rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]
      exact ⟨y_in, fun j _ => by simpa using hz j⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t

Tactic:
rw [← sInter_singleton s, sInter_prod_sInter (singleton_nonempty s) hT, sInter_singleton]

Goal state after:
α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂ r ∈ {s} ×ˢ T, r.1 ×ˢ r.2 = ⋂ t ∈ T, s ×ˢ t
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
b : α
⊢ {1 * b⁻¹} = {b⁻¹}

Tactic:
one_mul

Goal state after:
α : Type u_2
inst✝ : Group α
b : α
⊢ {b⁻¹} = {b⁻¹}
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 y = 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 y
Module: Mathlib.Algebra.Group.Subgroup.Lattice

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

Tactic:
simp only [ne_eq, Subtype.exists, mk_eq_one, exists_prop]

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

Tactic:
one_mul

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
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⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : x / y ∈ f.ker
⊢ 1 * f y = f y

Tactic:
one_mul

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : x / y ∈ f.ker
⊢ f y = f y
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < b₂ * b₂ + a

Tactic:
rw [Nat.add_comm, Nat.add_comm _ a, Nat.add_assoc, Nat.add_lt_add_iff_left]

Goal state after:
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ b₁ + a * a < b₂ * b₂
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a b : α
s : Set α
⊢ a ∈ b • s⁻¹ ↔ b ∈ a • s

Tactic:
by
  simp [mem_smul_set_iff_inv_smul_mem]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
⊢ a = 1

Tactic:
have ⟨q, eq⟩ := h.exists_left_inv

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
q : M
eq : q * a = 1
⊢ a = 1
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ (hd :: tl).prod

Tactic:
rw [prod_cons]

Goal state after:
case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ tl.prod
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ hd * tl.prod
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case inl.inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ 1 * 1 ∈ {1, a}

Tactic:
one_mul

Goal state after:
case inl.inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ 1 ∈ {1, a}