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
a : k
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋

Tactic:
refine mul_lt_floor ?_ ?_ ?_

Goal state after:
case refine_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 0 < 2⁻¹

case refine_2
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 2⁻¹ < 1

case refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ ↑⌈2⁻¹ / (1 - 2⁻¹)⌉ ≤ a
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : ¬a ∈ s
⊢ count a s = 0

Tactic:
exact count_eq_zero_of_notMem h

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

Goal state before:
pp: case mp
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) → m ≤ replicate n x

pp: case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ m ≤ replicate n x → ∃ a, a ::ₘ m ≤ replicate (n + 1) x

Tactic:
· rintro ⟨x', hx'⟩
    have := eq_of_mem_replicate (mem_of_le hx' (mem_cons_self _ _))
    rwa [this, replicate_succ, cons_le_cons_iff] at hx'

Goal state after:
case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ m ≤ replicate n x → ∃ a, a ::ₘ m ≤ replicate (n + 1) x
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
j : Fin l.length
i : ℕ
hi : i < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) j
⊢ ⟨i, hi⟩ = j

Tactic:
obtain ⟨j, hj⟩ := j

Goal state after:
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
f f' : α → β
hf : ∀ (a : α), a ∈ m → f a = f' a
⊢ map f m ≍ map f' m

Tactic:
simp [map_congr rfl hf]

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

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬x ∈ tl ∧ tl.Nodup
⊢ (update f x y x :: if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl) =
    if x = x ∨ x ∈ tl then (f x :: map f tl).set (idxOf x (x :: tl)) y else f x :: map f tl

Tactic:
simp [hl.1]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this : 0 < count a l'
⊢ False

Tactic:
have : count a l.dedup ≤ 1 := nodup_iff_count_le_one.1 (nodup_dedup l) a

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this✝ : 0 < count a l'
this : count a l.dedup ≤ 1
⊢ False
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : head✝ ∈ l₂
⊢ head✝ :: tail✝.bagInter (l₂.erase head✝) <+ (head✝ :: tail✝) ∩ l₂

pp: case cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : ¬head✝ ∈ l₂
⊢ tail✝.bagInter l₂ <+ (head✝ :: tail✝) ∩ l₂

Tactic:
· rw [inter_cons_of_mem _ (by assumption), cons_sublist_cons]
      exact ih.trans <| Sublist.inter_left (by grind [erase_sublist])

Goal state after:
case cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : ¬head✝ ∈ l₂
⊢ tail✝.bagInter l₂ <+ (head✝ :: tail✝) ∩ l₂
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ t.inits
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ a :: r <+: a :: t

Tactic:
← ht

Goal state after:
α : Type u_1
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ t.inits
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ a :: r <+: a :: (r ++ s)
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
m : Multiset α
hm : m.Nodup
⊢ { val := m, nodup := hm }.Nonempty ↔ m ≠ 0

Tactic:
induction m using Multiset.induction_on

Goal state after:
case empty
α : Type u_1
hm : Nodup 0
⊢ { val := 0, nodup := hm }.Nonempty ↔ 0 ≠ 0

case cons
α : Type u_1
a✝¹ : α
s✝ : Multiset α
a✝ : ∀ {hm : s✝.Nodup}, { val := s✝, nodup := hm }.Nonempty ↔ s✝ ≠ 0
hm : (a✝¹ ::ₘ s✝).Nodup
⊢ { val := a✝¹ ::ₘ s✝, nodup := hm }.Nonempty ↔ a✝¹ ::ₘ s✝ ≠ 0
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:
by simp +contextual [subset_iff, h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
⊢ insert a s \ insert b s = {a}

Tactic:
by
  ext; aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
hb : b ∈ s
⊢ s.erase a \ s.erase b = {b}

Tactic:
by
  ext; aesop

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

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
· rw [succAbove_of_le_castSucc _ _ h,
      succAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), rev_castSucc, rev_rev]

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

Goal state before:
pp: n : ℕ
j : Fin (n + 1)
⊢ ↑j + ↑j.rev = n

Tactic:
obtain ⟨j, hj⟩ := j

Goal state after:
n j : ℕ
hj : j < n + 1
⊢ ↑⟨j, hj⟩ + ↑⟨j, hj⟩.rev = n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = (m * n - (↑i / n * n + (↑i % n + 1))) % n

pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n ≤ (m - ↑i / n) * n

Tactic:
Nat.add_assoc

Goal state after:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + (↑i % n + 1))) % n = (m * n - (↑i / n * n + (↑i % n + 1))) % n

n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n ≤ (m - ↑i / n) * n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case zero
a b : Fin (0 + 1)
h : a < b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

pp: case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

Tactic:
· lia

Goal state after:
case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
by
  rw [succ_castPred_eq_castPred_succ ha, lt_castPred_succ_iff]

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

Goal state before:
pp: α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∃! a, p a) ↔ ∃ a, {x | p x} = {a}

Tactic:
refine exists_congr fun x => ?_

Goal state after:
α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ ((fun a ↦ p a) x ∧ ∀ (y : α), (fun a ↦ p a) y → y = x) ↔ {x | p x} = {x}
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ card { x // ¬p x } = card α - card { x // p x }

Tactic:
by
  classical
    rw [Fintype.card_of_subtype (Set.toFinset { x | p x }ᶜ), Set.toFinset_compl,
      Finset.card_compl, Fintype.card_of_subtype] <;>
    · intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_ofPred]

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

Goal state before:
pp: m n : ℕ
α : Fin (n + 1) → Sort u_1
x✝ : α (last n)
q : (i : Fin (n + 1)) → α i
p✝ : (i : Fin n) → α i.castSucc
i✝ : Fin n
y : α i✝.castSucc
z : α (last n)
p : (i : Fin n) → α i.castSucc
x : α (last n)
i : Fin (n + 1)
h : ¬↑i < n
⊢ α (last n) = α i

Tactic:
eq_last_of_not_lt h

Goal state after:
m n : ℕ
α : Fin (n + 1) → Sort u_1
x✝ : α (last n)
q : (i : Fin (n + 1)) → α i
p✝ : (i : Fin n) → α i.castSucc
i✝ : Fin n
y : α i✝.castSucc
z : α (last n)
p : (i : Fin n) → α i.castSucc
x : α (last n)
i : Fin (n + 1)
h : ¬↑i < n
⊢ α (last n) = α (last n)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
hG : Antitone fun i ↦ #(g i) - 1
⊢ ∃ n < #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s

Tactic:
rcases Nat.stabilises_of_antitone hG (by grind [=_ image_image, iterate_succ']) with ⟨n, hn, hn'⟩

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
hG : Antitone fun i ↦ #(g i) - 1
n : ℕ
hn : n ≤ #(g 0) - 1
hn' : ∀ (m : ℕ), n ≤ m → #(g m) - 1 = #(g n) - 1
⊢ ∃ n < #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j

Tactic:
eq_last_of_not_lt h

Goal state after:
case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) (last n) = snoc (g ∘ q) (g y) (last n)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : i < l.length
hj : ¬j < l.length
⊢ ↑(f ⟨i, hi⟩) < j + l'.length

pp: case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : j < l.length
⊢ i + l'.length < ↑(f ⟨j, hj⟩)

pp: case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : ¬j < l.length
⊢ i + l'.length < j + l'.length

Tactic:
· lia

Goal state after:
case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : j < l.length
⊢ i + l'.length < ↑(f ⟨j, hj⟩)

case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : ¬j < l.length
⊢ i + l'.length < j + l'.length
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ insertNth 0 x p = cons x fun j ↦ cast ⋯ (p j)

Tactic:
refine insertNth_eq_iff.2 ⟨by simp, ?_⟩

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ p = removeNth 0 (cons x fun j ↦ cast ⋯ (p j))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
⊢ (last n).insertNth x p = snoc (fun j ↦ cast ⋯ (p j)) x

Tactic:
refine insertNth_eq_iff.2 ⟨by simp, ?_⟩

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
⊢ p = (last n).removeNth (snoc (fun j ↦ cast ⋯ (p j)) x)
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

Tactic:
by
    by_cases h : a ∈ s; swap; · simp [IH, h]
    simp only [h, dedup_cons_of_mem, IH, fold_cons_left]
    show fold op b s = op a (fold op b s)
    rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_3
m : (i : Fin (n + 2)) → α i
i : Fin (n + 1)
j : Fin (n + 2)
⊢ i.removeNth (j.removeNth m) ≍ (i.predAbove j).removeNth ((j.succAbove i).removeNth m)

Tactic:
by
  apply Function.hfunext rfl
  simp only [heq_iff_eq]
  rintro k _ rfl
  unfold removeNth
  apply congr_arg_heq
  rw [succAbove_succAbove_succAbove_predAbove]

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.rotate l.length = l

Tactic:
rw [rotate_eq_rotate', rotate'_length]

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

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
ih : op xs.prod = (map op xs).reverse.prod
⊢ op (x :: xs).prod = (map op (x :: xs)).reverse.prod

Tactic:
List.prod_cons,

Goal state after:
case cons
M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
ih : op xs.prod = (map op xs).reverse.prod
⊢ op (x * xs.prod) = (map op (x :: xs)).reverse.prod
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ s ≤ s.card • t ↔ s ⊆ t

Tactic:
refine ⟨fun hle ↦ Subset.trans (subset_of_le hle) (t.smul_subset_self s.card), ?_⟩
  refine fun hsub ↦ le_iff_count.mpr fun a ↦ ?_
  by_cases! has : a ∉ s
  · simp [count_eq_zero_of_notMem has]
  grw [count_le_card, count_nsmul, ← one_le_count_iff_mem.mpr <| mem_of_subset hsub has, mul_one]

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

Goal state before:
pp: α : Type u_1
s : Finset α
x : α × α
⊢ x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2

Tactic:
rcases s with ⟨⟨s⟩, hs⟩
  exact hs.mem_offDiag

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

Goal state before:
pp: n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose k + n.multichoose (k + 1) = (n + (k + 1)).choose (k + 1)

Tactic:
← Nat.add_assoc,

Goal state after:
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose k + n.multichoose (k + 1) = (n + k + 1).choose (k + 1)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Injective f ↔ ∀ (i : ι), Injective ((U i).restrictPreimage f)

Tactic:
refine ⟨fun H i => (U i).restrictPreimage_injective H, fun H x y e => ?_⟩
  obtain ⟨i, hi⟩ := Set.mem_iUnion.mp
      (show f x ∈ Set.iUnion U by rw [hU]; trivial)
  injection @H i ⟨x, hi⟩ ⟨y, show f y ∈ U i from e ▸ hi⟩ (Subtype.ext e)

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
s : Set M
inst✝ : MulOneClass N
f g : M →* N
⊢ 1 = g 1

Tactic:
g.map_one

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
s : Set M
inst✝ : MulOneClass N
f g : M →* N
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

pp: case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
⊢ (∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1

Tactic:
· have hst : (s * t).Nonempty := h.symm.subst one_nonempty
    obtain ⟨a, ha⟩ := hst.of_image2_left
    obtain ⟨b, hb⟩ := hst.of_image2_right
    have H : ∀ {a b}, a ∈ s → b ∈ t → a * b = (1 : α) := fun {a b} ha hb =>
      h.subset <| mem_image2_of_mem ha hb
    refine ⟨a, b, ?_, ?_, H ha hb⟩ <;> refine eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩
    · exact (eq_inv_of_mul_eq_one_left <| H hx hb).trans (inv_eq_of_mul_eq_one_left <| H ha hb)
    · exact (eq_inv_of_mul_eq_one_right <| H ha hx).trans (inv_eq_of_mul_eq_one_right <| H ha hb)

Goal state after:
case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
⊢ (∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1) → s * t = 1
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ s ⊆ s / t

Tactic:
div_eq_mul_inv

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ s ⊆ s * t⁻¹
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ s ⊆ s / t

Tactic:
by
  rw [div_eq_mul_inv]; exact subset_mul_left _ <| by simpa

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s / t

Tactic:
div_eq_mul_inv

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor
  · contrapose! +distrib
    rintro (hs | rfl)
    · exact hs.zpow
    · simp
  · rintro ⟨rfl, hn⟩
    exact empty_zpow hn

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

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x / y ∈ H

Tactic:
div_eq_mul_inv

Goal state after:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x * y⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Defs

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

Tactic:
by
  rw [← inv_mem_iff, mem_set_normalizer_iff, inv_inv]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
s : Set N
x : G
hx : x ∈ ⇑f ⁻¹' s
⊢ x ∈ ↑(comap f (closure s))

Tactic:
by rw [SetLike.mem_coe, mem_comap]; exact subset_closure hx

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g h : G
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x = h * g) ↔ h ∈ s)

Tactic:
← eq_inv_mul_iff_mul_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g h : G
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, x = g⁻¹ * (h * g)) ↔ h ∈ s)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x

Tactic:
conjugatesOfSet,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ ⋃ a ∈ s, conjugatesOf a ↔ ∃ a ∈ s, IsConj a x
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_5
inst✝ : Group G
s t : Set G
⊢ conjugatesOfSet (s ∪ t) = conjugatesOfSet s ∪ conjugatesOfSet t

Tactic:
conjugatesOfSet,

Goal state after:
G : Type u_5
inst✝ : Group G
s t : Set G
⊢ ⋃ a ∈ s ∪ t, conjugatesOf a = (⋃ a ∈ s, conjugatesOf a) ∪ ⋃ a ∈ t, conjugatesOf a
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : 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

Tactic:
div_eq_mul_inv

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
N : Type u_5
inst✝² : Group N
G' : Type u_8
N' : Type u_9
inst✝¹ : Group G'
inst✝ : Group N'
f : G →* N
g : G' →* N'
⊢ comap (f.prodMap g) ⊥ = (comap f ⊥).prod (comap g ⊥)

Tactic:
← prodMap_comap_prod,

Goal state after:
G : Type u_1
inst✝³ : Group G
N : Type u_5
inst✝² : Group N
G' : Type u_8
N' : Type u_9
inst✝¹ : Group G'
inst✝ : Group N'
f : G →* N
g : G' →* N'
⊢ comap (f.prodMap g) ⊥ = comap (f.prodMap g) (⊥.prod ⊥)
Module: Mathlib.Algebra.Group.Subgroup.Basic

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
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ g.ker

Tactic:
apply hg

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
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ f.ker
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f_inv (f x) * x⁻¹ ∈ g.ker

Tactic:
apply hg

Goal state after:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f_inv (f x) * x⁻¹ ∈ f.ker
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Monoid M
f g : FreeMonoid α →* M
h : ∀ (x : α), f (of x) = g (of x)
l : FreeMonoid α
x : α
xs : FreeMonoid α
hxs : f xs = g xs
⊢ f (of x * xs) = g (of x * xs)

Tactic:
simp only [h, hxs, map_mul]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
f : α → M
x✝¹ x✝ : FreeMonoid α
⊢ prodAux (List.map f (toList (x✝¹ * x✝))) = prodAux (List.map f (toList x✝¹)) * prodAux (List.map f (toList x✝))

Tactic:
simp only [prodAux_eq, toList_mul, List.map_append, List.prod_append]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
⊢ ∀ (a : Lex (α × β)), ∃ b, a < b

Tactic:
rw [Lex.forall, Prod.forall]
    intro a b
    obtain ⟨c, h⟩ := exists_gt a
    use toLex (c, b)
    simpa [lt_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
a : α
l : List α
⊢ argmax f (l ++ [a]) = Option.casesOn (argmax f l) (some a) fun c ↦ if f c < f a then some a else some c

Tactic:
rw [argmax, argmax]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
a : α
l : List α
⊢ foldl (argAux fun b c ↦ f c < f b) none (l ++ [a]) =
    Option.casesOn (foldl (argAux fun b c ↦ f c < f b) none l) (some a) fun c ↦ if f c < f a then some a else some c
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithBot α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ↑a ≤ b) → l.maximum ≤ b
h : ∀ (a_1 : α), a_1 ∈ a :: l → ↑a_1 ≤ b
⊢ (a :: l).maximum ≤ b

Tactic:
simp only [maximum_cons, max_le_iff]

Goal state after:
case cons
α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithBot α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ↑a ≤ b) → l.maximum ≤ b
h : ∀ (a_1 : α), a_1 ∈ a :: l → ↑a_1 ≤ b
⊢ ↑a ≤ b ∧ l.maximum ≤ b
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.max' ⋯ = a

Tactic:
by simp [max']

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (s.sup fun i ↦ a ⊓ f i) = s.sup fun i ↦ f i ⊓ a

Tactic:
simp_rw [_root_.inf_comm]

Goal state after: