mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℕ
m0 : 0 < m
⊢ n * 1 ≤ n * 1 * m

Tactic:
mul_one

Goal state after:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℕ
m0 : 0 < m
⊢ n ≤ n * m
Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t

Tactic:
by
  ext; simp [mem_smul, mem_smul_set, h]

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t ↔ s ≤ t

Tactic:
refine ⟨?_, fun h => le_trans h <| le_cons_self _ _⟩
  suffices ∀ {t'}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t' by
    exact fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))
  introv h
  revert m
  refine leInductionOn h ?_
  introv s m₁ m₂
  rcases append_of_mem m₂ with ⟨r₁, r₂, rfl⟩
  exact
    perm_middle.subperm_left.2
      ((subperm_cons _).2 <| ((sublist_or_mem_of_sublist s).resolve_right m₁).subperm)

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl₁ : l₁.Nodup
⊢ a ∈ List.filter (fun x ↦ decide ¬x ∈ l₂) l₁ ↔ a ∈ l₁ ∧ ¬a ∈ l₂

Tactic:
mem_filter,

Goal state after:
α : Type u
l₁ l₂ : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl₁ : l₁.Nodup
⊢ a ∈ l₁ ∧ (decide ¬a ∈ l₂) = true ↔ a ∈ l₁ ∧ ¬a ∈ l₂
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
hp : ∃! a, a ∈ ⟦b⟧ ∧ p a
⊢ Eq.ndrec (motive := fun x ↦ (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a }) (fun ex_unique ↦ List.chooseX p a ⋯) ⋯ hp =
    List.chooseX p b ⋯

Tactic:
suffices all_equal : ∀ x y : { t // t ∈ b ∧ p t }, x = y by
        apply all_equal

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
hp : ∃! a, a ∈ ⟦b⟧ ∧ p a
⊢ ∀ (x y : { t // t ∈ b ∧ p t }), x = y
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
a : α
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p {a} = if p a then {a} else ∅

Tactic:
by
  simp only [singleton, filter_cons, filter_zero, Multiset.add_zero, empty_eq_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.toFinset ⊆ t.toFinset ∧ ¬t.toFinset ⊆ s.toFinset ↔ s ⊂ t

Tactic:
toFinset_subset

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ⊆ t ∧ ¬t ⊆ s ↔ s ⊂ t
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.val.toFinset = s

Tactic:
by
  ext
  rw [Multiset.mem_toFinset, ← mem_def]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
l : Multiset α
d : l.Nodup
⊢ a ∈ Multiset.filter (fun x ↦ x ≠ b) l ↔ a ≠ b ∧ a ∈ l

Tactic:
mem_filter,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : Multiset α
d : l.Nodup
⊢ a ∈ l ∧ a ≠ b ↔ a ≠ b ∧ a ∈ l
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case cons.cons
α : Type u_1
tail✝¹ : List α
ih : ∀ {l₁ : List α}, l₁ <+: tail✝¹ → tail✝¹ = l₁ ++ drop l₁.length tail✝¹
head✝ : α
tail✝ : List α
h' : tail✝ <+: tail✝¹
h : head✝ :: tail✝ <+: head✝ :: tail✝¹
⊢ head✝ :: tail✝¹ = head✝ :: tail✝ ++ drop (head✝ :: tail✝).length (head✝ :: tail✝¹)

Tactic:
simpa using ih h'

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ insert a l = if a ∈ l then l else a :: l

Tactic:
simp only [← elem_iff]
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
h : (image f s).Nontrivial
⊢ s.Nontrivial

Tactic:
simp only [Finset.Nontrivial, coe_image] at h ⊢
  exact Set.nontrivial_of_image _ _ h

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ image (fun i ↦ f i) (range n) → a ∈ Set.range f

Tactic:
· rintro h
    simp only [mem_image, Set.mem_range, mem_range] at *
    rcases h with ⟨i, _, ha⟩
    exact ⟨i, ha⟩

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

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

Tactic:
wlog! h : i < j generalizing i j

Goal state after:
case inr
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
h : j ≤ i
⊢ i = j

n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
h : i < j
⊢ i = j
Module: Mathlib.Data.Fin.Basic

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

Tactic:
by
  omega

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

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ i.pred hi ≤ j ↔ i ≤ j.succ

Tactic:
by
  rw [← succ_le_succ_iff, succ_pred]

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

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j ≤ i.pred hi ↔ j.succ ≤ i

Tactic:
by
  rw [← succ_le_succ_iff, succ_pred]

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

Goal state before:
pp: α : Type u
n : ℕ
c : α
⊢ (ofFn fun x ↦ c) = replicate (n + 1) c

Tactic:
by rw [replicate, ← ofFn_const n]; simp

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

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
h : a ≠ last (n + 1)
⊢ a.succAbove (last n) = last (n + 1)

Tactic:
by
  rw [succAbove_of_lt_succ _ _ (succ_last _ ▸ lt_last_iff_ne_last.2 h), succ_last]

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

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
⊢ a.succAbove b = last (n + 1) ↔ b = last n

Tactic:
rw [← succAbove_ne_last_last ha, succAbove_right_inj]

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

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ map (⇑σ) (finRange n) ~ finRange n

Tactic:
by
  rw [perm_ext_iff_of_nodup ((nodup_finRange n).map σ.injective) <| nodup_finRange n]
  simpa [mem_map, mem_finRange] using! σ.surjective

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Nonempty α
⊢ #s ≤ 1 ↔ ∃ x, s ⊆ {x}

Tactic:
by
  refine ⟨fun H => ?_, ?_⟩
  · obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
    · exact ⟨Classical.arbitrary α, empty_subset _⟩
    · exact ⟨x, fun y hy => by rw [card_le_one.1 H y hy x hx, mem_singleton]⟩
  · rintro ⟨x, hx⟩
    rw [← card_singleton x]
    exact card_le_card hx

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
⊢ init (update q i.castSucc y) = update (init q) i y

Tactic:
by
  ext j
  by_cases h : j = i
  · rw [h]
    simp [init]
  · simp [init, h, castSucc_inj]

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)
motive : ((i : Fin n.succ) → α i) → Sort u_2
snoc : (xs : (i : Fin n) → α i.castSucc) → (x : α (last n)) → motive (Fin.snoc xs x)
x : (i : Fin n.succ) → α i
⊢ motive (Fin.snoc (init x) (x (last n))) = motive x

Tactic:
Fin.snoc_init_self

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)
motive : ((i : Fin n.succ) → α i) → Sort u_2
snoc : (xs : (i : Fin n) → α i.castSucc) → (x : α (last n)) → motive (Fin.snoc xs x)
x : (i : Fin n.succ) → α i
⊢ motive x = motive x
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
k : Fin n
hk : (i.succAbove j).castPred H₁ = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j

Tactic:
castPred_succAbove _ _ hlt

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s ≤ c ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c

Tactic:
change _ ≥ _ ↔ _
  apply fold_op_rel_iff_or
  intro x y z
  change _ ≤ _ ↔ _
  exact min_le_iff

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

Goal state before:
pp: case refine_1
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b ∨ a = b ∧ Lex r l₁ l₂
⊢ Lex r (a :: l₁) (b :: l₂)

Tactic:
rcases h with (h | ⟨rfl, h⟩)
      · exact Lex.rel h
      · exact Lex.cons h

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

Goal state before:
pp: case cons.cons
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
b : α
l₂ : List α
H : (head✝ :: tail✝).length ≤ (b :: l₂).length
h : head✝ :: tail✝ ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) (b :: l₂)

Tactic:
case cons.cons a l₁ IH =>
      by_cases ab : a = b
      · subst b
        exact .cons <| IH (le_of_succ_le_succ H) (mt (congr_arg _) h)
      · exact .rel ab

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

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ (take (n % (a :: l).length) (a :: l)).prod * 1 = (take (n % (a :: l).length) (a :: l)).prod

Tactic:
mul_one

Goal state after:
G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ (take (n % (a :: l).length) (a :: l)).prod = (take (n % (a :: l).length) (a :: l)).prod
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
a : α
n : ℕ
⊢ replicate (n * 1) a = replicate n a

Tactic:
mul_one

Goal state after:
α : Type u_1
a : α
n : ℕ
⊢ replicate n a = replicate n a
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
b : α
hb : b ∈ n • {a}
⊢ p b

Tactic:
rwa [mem_singleton.mp (mem_of_mem_nsmul hb)]

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

Goal state before:
pp: case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
b : α
hb : b ∈ n • {a}
⊢ ¬p b

Tactic:
rwa [mem_singleton.mp (mem_of_mem_nsmul hb)]

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

Goal state before:
pp: case neg
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : a ∈ s
⊢ s.card ≤ s.card * 1

Tactic:
mul_one

Goal state after:
case neg
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
has : a ∈ s
⊢ s.card ≤ s.card
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
        (Disjoint ((insert a s).biUnion f) t ↔ ∀ i ∈ insert a s, Disjoint (f i) t)

Tactic:
intro i s his ih

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s✝ : Finset α
f : α → Finset β
t : Finset β
i : α
s : Finset α
his : i ∉ s
ih : Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t
⊢ Disjoint ((insert i s).biUnion f) t ↔ ∀ i_1 ∈ insert i s, Disjoint (f i_1) t
Module: Mathlib.Data.Fintype.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
H : Infinite (α × β)
⊢ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

Tactic:
rw [and_comm]

Goal state after:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ⇑{ toFun := Prod.swap, inj' := ⋯ } '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t

Tactic:
exact Set.image_swap_prod _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ Prod.swap '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t

Tactic:
exact Set.image_swap_prod _ _

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

Goal state before:
pp: case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 2 (k + 1) = k + 1 + 1

Tactic:
rw [multichoose, IH]; simp [Nat.add_comm]

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ s⁻¹.Finite ↔ s.Finite

Tactic:
by
  rw [← image_inv_eq_inv, finite_image_iff inv_injective.injOn]

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

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

Tactic:
mul_one

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
x✝ : IsConj 1 a
c : αˣ
h : ↑c * 1 = a * ↑c
⊢ a = 1

Tactic:
mul_one

Goal state after:
α : Type u
inst✝ : Monoid α
a : α
x✝ : IsConj 1 a
c : αˣ
h : ↑c = a * ↑c
⊢ a = 1
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : MulOneClass M
s : Set M
S : Submonoid M
a✝ b✝ : M
hb : b✝ = 1
ha : a✝ = 1
⊢ 1 * 1 = 1

Tactic:
mul_one

Goal state after:
M : Type u_1
N : Type u_2
inst✝ : MulOneClass M
s : Set M
S : Submonoid M
a✝ b✝ : M
hb : b✝ = 1
ha : a✝ = 1
⊢ 1 = 1
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
⊢ x default ∈ s i

Tactic:
rw [this]
    apply hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
⊢ f '' ⋃₀ s = ⋃₀ (image f '' s)

Tactic:
by
  ext
  simp only [Set.mem_iUnion, Set.sUnion_image]
  grind

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ op '' s⁻¹ = (op '' s)⁻¹

Tactic:
simp_rw [← image_inv_eq_inv, Function.Semiconj.set_image op_inv s]

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n✝ n : ℕ
hn : n + 1 ≠ 0
⊢ ∅ ^ (n + 1) = ∅

Tactic:
by simp [pow_succ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
s : Set (α → β)
t : Set α
⊢ f '' s.seq t = ((fun x ↦ f ∘ x) '' s).seq t

Tactic:
by
  simp only [seq, image_image2, image2_image_left, comp_apply]

Goal state after:
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:
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✝ : Group α
a : α
⊢ {a⁻¹ * 1} = {a⁻¹}

Tactic:
mul_one

Goal state after:
α : Type u_2
inst✝ : Group α
a : α
⊢ {a⁻¹} = {a⁻¹}
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : ∃ g, ↑H = {g}
g : G
hg : ↑H = {g}
⊢ Subsingleton ↑↑H

Tactic:
rw [hg]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : ∃ g, ↑H = {g}
g : G
hg : ↑H = {g}
⊢ Subsingleton ↑{g}
Module: Mathlib.Algebra.Group.Subgroup.Ker

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

Tactic:
mul_one

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : y⁻¹ * x ∈ f.ker
⊢ f y = f y
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: S : Type u_3
inst✝ : Semigroup S
a b : S
hab : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ a * b * (a * b) = a * b

Tactic:
hab.symm.mul_mul_mul_comm,

Goal state after:
S : Type u_3
inst✝ : Semigroup S
a b : S
hab : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ a * a * (b * b) = a * b
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ ⋃ g, g • s = {a | ∃ g, g • a ∈ s}

Tactic:
← iUnion_ofPred,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ ⋃ g, g • s = ⋃ i, {x | i • x ∈ s}
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 (f_inv (f x)) * (f x)⁻¹ = 1

Tactic:
mul_inv_eq_one

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 (f_inv (f x)) = f x
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * 1 = of d
H : (map f) a✝¹ = 1
⊢ f head = d

Tactic:
mul_one

Goal state after:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) = of d
H : (map f) a✝¹ = 1
⊢ f head = d
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * (a * 1) ∈ H
⊢ b * a ∈ H

Tactic:
mul_one

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * a ∈ H
⊢ b * a ∈ H
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons.inr
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : ∃ a, a ∈ l ∧ f a < g a
⊢ f i * (map f l).prod < g i * (map g l).prod

Tactic:
exact mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›

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

Goal state before:
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
⊢ x * 1 = x

Tactic:
mul_one

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
⊢ x = x
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
⊢ toLex (a₁, b₁) ⋖ toLex (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ ⋖ b₂ ∨ a₁ ⋖ a₂ ∧ IsMax b₁ ∧ IsMin b₂

Tactic:
simp only [CovBy, toLex_lt_toLex, toLex.surjective.forall, Prod.forall, isMax_iff_forall_not_lt,
    isMin_iff_forall_not_lt]
  grind

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

Goal state before:
pp: case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : AddMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
l : List α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
hd : α
tl : List α
IH : f tl.prod ≤ (map f tl).sum
⊢ f (hd :: tl).prod ≤ (map f (hd :: tl)).sum

Tactic:
grw [prod_cons, h_mul, IH]

Goal state after:
case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : AddMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
l : List α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
hd : α
tl : List α
IH : f tl.prod ≤ (map f tl).sum
⊢ f hd + (map f tl).sum ≤ (map f (hd :: tl)).sum
Module: Mathlib.Algebra.Group.Submonoid.Membership

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

Tactic:
mul_one

Goal state after:
case inr.inl
M : Type u_1
inst✝ : Monoid M
a✝ : M
ha : IsIdempotentElem a✝
⊢ a✝ ∈ {1, a✝}
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x✝ : M
n : ℕ
hpos : 0 < n
hx : x✝ ^ n = 1
m : ℕ
x : ↥(powers x✝)
⊢ x ^ Int.negSucc m = (x ^ ↑m.succ) ^ (n - 1)

Tactic:
change x ^ (Int.natMod _ n) = (x ^ (Int.natMod _ n)) ^ (n - 1)

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x✝ : M
n : ℕ
hpos : 0 < n
hx : x✝ ^ n = 1
m : ℕ
x : ↥(powers x✝)
⊢ x ^ (Int.negSucc m).natMod ↑n = (x ^ (↑m.succ).natMod ↑n) ^ (n - 1)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x) = ↑(Submonoid.powers (Multiplicative.ofAdd x))

Tactic:
by
  symm
  rw [Equiv.eq_image_iff_symm_image_eq]
  exact ofMul_image_powers_eq_multiples_ofMul

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
hn : n ∈ {y ∈ range ↑(ofNat s 0) | y ∈ s}
⊢ False

Tactic:
mem_filter,

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
hn : n ∈ range ↑(ofNat s 0) ∧ n ∈ s
⊢ False
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✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
f g : TopHom α β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by cases f; cases g; congr

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f g : SupHom α β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by cases f; cases g; congr

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a \ b) = f a \ f b

Tactic:
rw [sdiff_eq, sdiff_eq, map_inf, map_compl']

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

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

Tactic:
| insert a r _ ih =>

Goal state after: