mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Dedup

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

Tactic:
s.add_comm,

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

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

Tactic:
s.add_comm,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ t + s ∪ (u + s) = t + s ∪ (s + u)
Module: Mathlib.Data.Multiset.UnionInter

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

Tactic:
s.add_comm,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ (t + s) ∩ (u + s) = (t + s) ∩ (s + u)
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
h0 : count x M + count x N = count x P + count x Q
⊢ min (count x N) (count x Q) + (count x P - count x M) = count x N

Tactic:
omega

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ filter (fun x ↦ x = b) ⟦l⟧ = replicate (count b ⟦l⟧) b

Tactic:
simp only [quot_mk_to_coe, filter_coe, coe_count]
    rw [List.filter_eq, coe_replicate]

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

Goal state before:
pp: α : Type u_1
l : List α
m n : ℕ
⊢ min m l.length ≤ n ↔ m ≤ n ∨ l.length ≤ n

Tactic:
omega

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

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

Tactic:
rw [← cons_zero, toFinset_cons, toFinset_zero, LawfulSingleton.insert_empty_eq]

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

Goal state before:
pp: α : Type u_1
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), a ∈ s → p a → q a
⊢ filter p s ⊆ filter q s

Tactic:
simp +contextual [subset_iff, h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s.erase a ⊆ (insert a s).erase a

Tactic:
by grw [← subset_insert]

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

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

Tactic:
rw [← Finset.coe_ssubset, coe_toFinset]

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

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

Tactic:
rw [← Finset.coe_ssubset, coe_toFinset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
⊢ image f s = t ↔ Set.SurjOn f ↑s ↑t ∧ Set.MapsTo f ↑s ↑t

Tactic:
by
  grind [mapsTo_iff_image_subset, surjOn_iff_subset_image]

Goal state after:
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: m n k : Int
hn : 0 ≤ n
hk : 0 ≤ k
⊢ (m.fdiv n).fdiv k = m.fdiv (n * k)

Tactic:
by
  rw [Int.fdiv_eq_ediv_of_nonneg _ hn,
    Int.fdiv_eq_ediv_of_nonneg _ hk,
    Int.fdiv_eq_ediv_of_nonneg _ (Int.mul_nonneg hn hk),
    ediv_ediv_of_nonneg hn]

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

Goal state before:
pp: case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑(n - ↑v + ↑u) - ↑n = ↑↑u - ↑↑v

Tactic:
omega

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

Goal state before:
pp: case isTrue.H1
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ 0 ≤ ↑(n - ↑v + ↑u) - ↑n

Tactic:
omega

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

Goal state before:
pp: case isTrue.H2
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑(n - ↑v + ↑u) - ↑n < ↑n

Tactic:
omega

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

Goal state before:
pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑(n - ↑v + ↑u) = ↑↑u - ↑↑v + ↑n

Tactic:
omega

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

Goal state before:
pp: case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ 0 ≤ ↑(n - ↑v + ↑u)

Tactic:
omega

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

Goal state before:
pp: case isFalse.H2
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑(n - ↑v + ↑u) < ↑n

Tactic:
omega

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i = j.predAbove i.succ
⊢ i = j

Tactic:
Fin.predAbove_of_le_castSucc _ _ (by simpa),

Goal state after:
n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i = i.succ.castPred ⋯
⊢ i = j
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isTrue.H1
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ 0 ≤ ↑↑u - ↑↑v

Tactic:
omega

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

Goal state before:
pp: case isTrue.H2
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑u - ↑↑v < ↑n

Tactic:
omega

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

Goal state before:
pp: case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ 0 ≤ ↑↑u - ↑↑v + ↑n

Tactic:
omega

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

Goal state before:
pp: case isFalse.H2
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑u - ↑↑v + ↑n < ↑n

Tactic:
omega

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
⊢ #s = n

Tactic:
have : s = (range n).attach.image fun i => f i.1 (mem_range.1 i.2) := by
    ext a
    suffices _ : a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a by
      simpa only [mem_image, mem_attach, true_and, Subtype.exists]
    constructor
    · intro ha; obtain ⟨i, hi, rfl⟩ := hf a ha; use i, mem_range.2 hi
    · rintro ⟨i, hi, rfl⟩; apply hf'

Goal state after:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun i ↦ f ↑i ⋯) (range n).attach
⊢ #s = n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ ↑↑(u + v) = (↑↑u + ↑↑v) % ↑n

Tactic:
omega

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

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a < n

Tactic:
omega

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

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ m - ↑b + ↑a < m

Tactic:
omega

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

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
h' : ↑a < ↑b
⊢ n - ↑b + ↑a = m - ↑b + ↑a + n - m

Tactic:
omega

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

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

Tactic:
rw [← card_sdiff_of_subset]

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

α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ∩ t ⊆ t
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
b : Fin n
ha : a ≠ 0
⊢ a.succAbove b = 0 ↔ b = 0

Tactic:
← succAbove_ne_zero_zero ha,

Goal state after:
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
b : Fin n
ha : a ≠ 0
⊢ a.succAbove b = a.succAbove 0 ↔ b = 0
Module: Mathlib.Data.Finset.Card

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

Tactic:
by
  rw [← card_union_of_disjoint (disjoint_sdiff_inter _ _), sdiff_union_inter]

Goal state after:
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
⊢ Function.Injective (Fin.cons x₀ xs)

Tactic:
Fin.cons_injective_iff

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 : (ofFn (Fin.cons x₀ xs)).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
hi : ¬i = last (n + 1)
⊢ (last n).predAbove i = i.castPred hi

Tactic:
· rw [predAbove_last_of_ne_last hi]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
t : Finset β
inst✝ : DecidableEq β
hf : Set.InjOn f ↑s
hf' : Set.MapsTo f ↑s ↑t
h : #t = #s + 1
⊢ ∃! x, x ∈ t ∧ x ∉ image f s

Tactic:
by
  have : #(t \ s.image f) = 1 := by
    grind [card_sdiff_of_subset hf'.finsetImage_subset, card_image_of_injOn hf]
  simpa [card_eq_one_iff_existsUnique] using this

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ append u v = v ∘ Fin.cast ⋯

Tactic:
by
  refine funext (Fin.addCases (fun l => ?_) fun r => ?_)
  · exact (Fin.cast hu l).elim0
  · rw [append_right, Function.comp_apply]
    refine congr_arg v (Fin.ext ?_)
    simp [hu]

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

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

Tactic:
rw [Subsingleton.elim i 0, Fin.append_right]

Goal state after:
case refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ x₀ 0 = snoc x (x₀ 0) (natAdd n 0)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
i : Fin n
hi : i.castSucc = last n
⊢ False

Tactic:
exact ne_last_of_lt i.castSucc_lt_last hi

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
⊢ insertionSort r (a :: l) = a :: insertionSort r l

Tactic:
rw [insertionSort_cons]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
⊢ orderedInsert r a (insertionSort r l) = a :: insertionSort r l
Module: Mathlib.Data.Set.Finite.Basic

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

Tactic:
h.coe_toFinset

Goal state after:
α : Type u
s : Set α
h : s.Finite
⊢ s.Nontrivial ↔ s.Nontrivial
Module: Mathlib.Data.List.Sort

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

Tactic:
exact (total_of r _ _).resolve_left h'

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✝ : List α
ih : ∀ {c : List α}, Pairwise r c → ∀ (d : List α), d ~ c → d <+ tail✝ → c <+ insertionSort r tail✝
c : List α
hs : Pairwise r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
⊢ c <+ insertionSort r (a :: tail✝)

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

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
⊢ Fin.find p h = 0 ↔ p 0

Tactic:
by simp [find_eq_iff]

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ p (Fin.find (fun k ↦ p k.succ) ⋯).succ ∧ ∀ (j : Fin (n + 1)), j < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p j

Tactic:
forall_fin_succ,

Goal state after:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ p (Fin.find (fun k ↦ p k.succ) ⋯).succ ∧
    (0 < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p 0) ∧
      ∀ (i : Fin n), i.succ < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p i.succ
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate n = [] ↔ l = []

Tactic:
by
  induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · simp [rotate_cons_succ, hn]

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

Goal state before:
pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse = (x :: l).reverse.rotate (x :: l).reverse.length

pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).reverse.length

pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length

Tactic:
rotate_length

Goal state after:
case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse = (x :: l).reverse

case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).reverse.length

case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length < (x :: l).reverse.length
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
← choose_succ_succ',

Goal state after:
n k : ℕ
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1) * (n + 1).choose (k + 1) + (n + 1).choose (k + 1)
Module: Mathlib.Algebra.Group.Subgroup.Map

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

Tactic:
by refine Subtype.image_preimage_coe _ _ |>.trans ?_; apply Set.inter_comm

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ comap f H ≤ f.ker ↔ Disjoint H f.range

Tactic:
← map_eq_bot_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ map f (comap f H) = ⊥ ↔ Disjoint H f.range
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
a b : ℕ
h : a < b
⊢ b ≤ pair a b

pp: case neg
a b : ℕ
h : ¬a < b
⊢ b ≤ pair a b

Tactic:
· simpa [pair, h] using le_trans (le_mul_self _) (Nat.le_add_right _ _)

Goal state after:
case neg
a b : ℕ
h : ¬a < b
⊢ b ≤ pair a b
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ pair a b₁ < pair a b₂

Tactic:
simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]
    by_cases h₂ : a < b₂; swap; · simp [h₂, h]
    simp only [h₂, ↓reduceIte]
    rw [Nat.add_comm, Nat.add_comm _ a, Nat.add_assoc, Nat.add_lt_add_iff_left]
    rwa [Nat.add_comm, ← sqrt_lt, sqrt_add_eq]
    exact le_trans (not_lt.mp h₁) (Nat.le_add_left _ _)

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
x✝ : (fun x ↦ x ∈ Set.range encode) x
n : α
hn : encode n = x
⊢ (decode₂ α x).isSome = true

Tactic:
rw [← hn, encodek₂]; exact rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ a * 1 ∈ H

Tactic:
← inv_one,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ a * 1⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x

Tactic:
smul_inter_nonempty_iff,

Goal state after:
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ∩ b • t ⊆ z • s⁻¹ * s ∩ (z • t⁻¹ * t)

Tactic:
by
      gcongr <;> apply smul_set_subset_mul <;> simpa

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ c⁻¹ * x * c ∈ N

pp: case refine_2
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h) ⟨c⁻¹ * x * c, ?refine_1⟩ = ⟨x, hx⟩

Tactic:
· have h := hn.conj_mem _ hx c⁻¹
      rwa [inv_inv] at h

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h) ⟨c⁻¹ * x * c, ⋯⟩ = ⟨x, hx⟩
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case inr.inl.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

Tactic:
· exact Or.inr (Lex.right _ _ hba)

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
a b : Lex (α × β)
this : DecidableLT (Lex (α × β))
⊢ ∀ {a b : Lex (α × β)}, compare a b = Ordering.eq ↔ (a == b) = true

Tactic:
simp [compare_def, compareLex, compareOn, Ordering.then_eq_eq]

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

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

Tactic:
by rw [Pi.inf_apply, map_top, map_top, inf_top_eq]

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

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ y :: l
hl : x ∈ l
⊢ a ≤ max y (foldr max b l)

Tactic:
exact le_max_of_le_right (IH hl)

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

Goal state before:
pp: case nil
α : Type u
init tail : List α
⊢ (init, tail) ∈ [].inits.zip [].tails ↔ init ++ tail = []

Tactic:
simp_rw [tails, inits, zip_cons_cons]

Goal state after:
case nil
α : Type u
init tail : List α
⊢ (init, tail) ∈ ([], []) :: [].zip [] ↔ init ++ tail = []
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {init tail : List α}, (init, tail) ∈ tail✝.inits.zip tail✝.tails ↔ init ++ tail = tail✝
init tail : List α
⊢ (init, tail) ∈ (head✝ :: tail✝).inits.zip (head✝ :: tail✝).tails ↔ init ++ tail = head✝ :: tail✝

Tactic:
simp_rw [tails, inits, zip_cons_cons]

Goal state after:
case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {init tail : List α}, (init, tail) ∈ tail✝.inits.zip tail✝.tails ↔ init ++ tail = tail✝
init tail : List α
⊢ (init, tail) ∈ ([], head✝ :: tail✝) :: (map (fun t ↦ head✝ :: t) tail✝.inits).zip tail✝.tails ↔
    init ++ tail = head✝ :: tail✝
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.mp.inl
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ a :: t

Tactic:
exact sublist_cons_of_sublist _ h

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ (powersetAux l).revzip ~ (powersetAux' l).revzip

Tactic:
have := Classical.decEq α
  rw [revzip_powersetAux_lemma l revzip_powersetAux, revzip_powersetAux_lemma l revzip_powersetAux']
  exact powersetAux_perm_powersetAux'.map _

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) (a :: l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)

Tactic:
rw [sublistsLen, sublistsLenAux, sublistsLenAux_eq, sublistsLenAux_eq, map_id,
      append_nil]

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (id ∘ cons a) (sublistsLen n l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
⊢ (∀ (n : κ), (f n).Pairwise r) → (⋃ n, f n).Pairwise r

Tactic:
intro H i hi j hj hij

Goal state after:
case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
⊢ r i j
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
t : Finset α
⊢ (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x

Tactic:
induction t using Finset.induction_on with
    | empty =>
      simpa only [forall_prop_of_true, and_true, forall_prop_of_false, bot_le, not_false_iff,
        sup_empty, forall_true_iff, notMem_empty]
    | insert a r _ ih =>
      intro h
      have incs : (r : Set α) ⊆ ↑(insert a r) := by
        rw [Finset.coe_subset]
        apply Finset.subset_insert
      -- x ∈ s is above the sup of r
      obtain ⟨x, ⟨hxs, hsx_sup⟩⟩ := ih fun x hx => h x <| incs hx
      -- y ∈ s is above a
      obtain ⟨y, hys, hay⟩ := h a (Finset.mem_insert_self a r)
      -- z ∈ s is above x and y
      obtain ⟨z, hzs, ⟨hxz, hyz⟩⟩ := hdir x hxs y hys
      use z, hzs
      rw [sup_insert, id, sup_le_iff]
      exact ⟨le_trans hay hyz, le_trans hsx_sup hxz⟩

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
t : Finset α
⊢ (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x

Tactic:
by
  classical
    induction t using Finset.induction_on with
    | empty =>
      simpa only [forall_prop_of_true, and_true, forall_prop_of_false, bot_le, not_false_iff,
        sup_empty, forall_true_iff, notMem_empty]
    | insert a r _ ih =>
      intro h
      have incs : (r : Set α) ⊆ ↑(insert a r) := by
        rw [Finset.coe_subset]
        apply Finset.subset_insert
      -- x ∈ s is above the sup of r
      obtain ⟨x, ⟨hxs, hsx_sup⟩⟩ := ih fun x hx => h x <| incs hx
      -- y ∈ s is above a
      obtain ⟨y, hys, hay⟩ := h a (Finset.mem_insert_self a r)
      -- z ∈ s is above x and y
      obtain ⟨z, hzs, ⟨hxz, hyz⟩⟩ := hdir x hxs y hys
      use z, hzs
      rw [sup_insert, id, sup_le_iff]
      exact ⟨le_trans hay hyz, le_trans hsx_sup hxz⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
hxt : x ⊆ t
hxn : #x = n
hsx : s ⊆ x
⊢ #(x \ s) = n - #s

Tactic:
by rw [card_sdiff_of_subset hsx, hxn]

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

Goal state before:
pp: α : Type u_1
a : α
o : Option α
⊢ a ∈ o.toFinset ↔ a ∈ o

Tactic:
by
  cases o <;> simp [eq_comm]

Goal state after: