mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i.rev = (p.rev.succAbove i).rev

Tactic:
rw [succAbove_rev_left, rev_rev]

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ (p.succAbove i).rev = p.rev.succAbove i.rev

Tactic:
rw [succAbove_rev_left, rev_rev]

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

Goal state before:
pp: case h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
this : e.symm ⟨j, ⋯⟩ < ⟨i, hi⟩
h : j = ↑(e.symm ⟨j, ⋯⟩)
⊢ j < i

Tactic:
rwa [h]

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

Goal state before:
pp: n : ℕ
j : Fin n
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
⊢ ∃ k, k ≠ ⟨i, hi⟩ ∧ k ≠ j

Tactic:
rcases j with ⟨j, hj⟩

Goal state after:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ ∃ k, k ≠ ⟨i, hi⟩ ∧ k ≠ ⟨j, hj⟩
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
⊢ Set.SurjOn f ↑s ↑t

Tactic:
by
  classical
  suffices s.image f = t by rw [Finset.surjOn_iff_subset_image, this]
  have : s.image f ⊆ t := hf.finsetImage_subset
  exact eq_of_subset_of_card_le this (hst.trans_eq (card_image_of_injOn hinj).symm)

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

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

Tactic:
lt_succAbove_iff_le_castSucc,

Goal state after:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p ≤ i.castSucc ↔ p < i.succ
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
by
  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
  · simp
  refine (Nat.succ_le_of_lt (card_pos.2 ⟨x, hx⟩)).ge_iff_eq'.trans (card_eq_one.trans ⟨?_, ?_⟩)
  · grind
  · exact fun h => ⟨x, by grind⟩

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

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : ¬i = 0
⊢ predAbove 0 i = i.pred hi

Tactic:
rw [predAbove_zero_of_ne_zero hi]

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

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

Tactic:
rw [hi, predAbove_right_last]

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

Goal state before:
pp: case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.castSucc < b
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

pp: case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

Tactic:
· rw [predAbove_of_castSucc_lt _ _ h, predAbove_castSucc_of_lt _ _ h,
      castSucc_pred_eq_pred_castSucc]

Goal state after:
case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype ↑(Set.range f)
x✝ : ↑(Set.range f)
val✝ : β
a : α
ha : f a = val✝
⊢ (fun a ↦ ⟨f a, ⋯⟩) a = ⟨val✝, ⋯⟩

Tactic:
simpa using ha

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

Goal state before:
pp: n : ℕ
α : Sort u_1
x : α
xs : Fin n → α
⊢ cons x xs = append (cons x elim0) xs ∘ Fin.cast ⋯

Tactic:
funext i

Goal state after:
n : ℕ
α : Sort u_1
x : α
xs : Fin n → α
i : Fin (n + 1)
⊢ cons x xs i = (append (cons x elim0) xs ∘ Fin.cast ⋯) i
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
⊢ α (i.castLT h).castSucc = α i

Tactic:
Fin.castSucc_castLT i 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
⊢ α i = α i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
⊢ snoc (init q) (q (last n)) j = q j

Tactic:
cases j using Fin.lastCases <;> simp [init]

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

Goal state before:
pp: m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
⊢ append (cons a as) bs = cons a (append as bs) ∘ Fin.cast ⋯

Tactic:
funext i

Goal state after:
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : Fin (n + 1 + m)
⊢ append (cons a as) bs i = (cons a (append as bs) ∘ Fin.cast ⋯) i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
⊢ append as (snoc bs b) = snoc (append as bs) b

Tactic:
funext i

Goal state after:
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : Fin (n + (m + 1))
⊢ append as (snoc bs b) i = snoc (append as bs) b i
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
by rintro (h | ⟨i, hi⟩) <;> exact ⟨_, ‹_›⟩

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

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

Tactic:
by rintro (h | ⟨i, hi⟩) <;> exact ⟨_, ‹_›⟩

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
hmn✝ : ¬m = n
hmn : m < n
⊢ natEmbeddingAux α m = Classical.choose ⋯

Tactic:
rw [h, natEmbeddingAux]

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ t
h : t ⊆ s
⊢ Fintype ↑t

Tactic:
rw [← inter_eq_self_of_subset_right h]
  apply Set.fintypeInterOfLeft

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

Goal state before:
pp: α : Sort u_3
n : ℕ
a : α
f : Fin n → α
⊢ cons a f ∘ rev = snoc (f ∘ rev) a

Tactic:
funext i

Goal state after:
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ (cons a f ∘ rev) i = snoc (f ∘ rev) a i
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l : List α
x✝² x✝¹ x✝ : α
⊢ decide (r x✝² x✝¹) = true → decide (r x✝¹ x✝) = true → decide (r x✝² x✝) = true

Tactic:
by simpa using trans_of r

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
f : Fin n → α
⊢ (ofFn f).SortedLE ↔ Monotone f

Tactic:
by
  simp only [sortedLE_iff_monotone_get, Monotone, Fin.forall_iff,
    length_ofFn, get_ofFn, Fin.cast_mk, Fin.mk_le_mk]

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

Goal state before:
pp: case inr.inr
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r b a
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

Tactic:
exact Or.inr (rel ab)

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

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

Tactic:
refine decidable_of_iff (r a b ∨ a = b ∧ Lex r l₁ l₂) ⟨fun h => ?_, fun h => ?_⟩

Goal state after:
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₂)

case refine_2
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r (a :: l₁) (b :: l₂)
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
b : α
l : List α
hl : List.IsChain (flip r) (a :: b :: l)
hl' : List.IsChain (flip r) (b :: l)
l' : List.chains r := ⟨b :: l, hl'⟩
⊢ Acc (List.lex_chains r) l'

Tactic:
· apply ih b (List.isChain_cons_cons.1 hl).1

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

Goal state before:
pp: case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate 0

pp: case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ n % l'.length ≤ l'.length

Tactic:
rotate_zero

Goal state after:
case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'

case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ n % l'.length ≤ l'.length
Module: Mathlib.Data.List.Rotate

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

Tactic:
rotate_zero

Goal state after:
α : Type u
l : List α
hl : l.Nodup
n : ℕ
⊢ l.rotate n = l ↔ l.rotate n = l
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
⊢ l ~r l' ↔ ∃ n, n ≤ l.length ∧ l.rotate n = l'

Tactic:
by
  refine ⟨fun h => ?_, fun ⟨n, _, h⟩ => ⟨n, h⟩⟩
  obtain ⟨n, rfl⟩ := h
  rcases l with - | ⟨hd, tl⟩
  · simp
  · refine ⟨n % (hd :: tl).length, ?_, rotate_mod _ _⟩
    refine (Nat.mod_lt _ ?_).le
    simp

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

Goal state before:
pp: α : Type u
l : List α
h : 0 < l.cyclicPermutations.length
⊢ l.rotate 0 = l

Tactic:
rotate_zero

Goal state after:
α : Type u
l : List α
h : 0 < l.cyclicPermutations.length
⊢ l = l
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case mpr
α : Type u
l : List α
k : ℕ
⊢ l ∈ (l.rotate k).cyclicPermutations

Tactic:
cyclicPermutations_rotate,

Goal state after:
case mpr
α : Type u
l : List α
k : ℕ
⊢ l ∈ l.cyclicPermutations.rotate k
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
have h₃ : k * n ! ≤ n * n ! := Nat.mul_le_mul_right _ (le_of_succ_le_succ hk)

Goal state after:
case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
⊢ n.choose a = n.choose b

Tactic:
rwa [h]

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset α
val✝ : Multiset α
s : List α
hs : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
⊢ Nodup (Quotient.map List.offDiag ⋯ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs }.val)

Tactic:
exact hs.offDiag

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · simp_rw [Set.Infinite, @and_comm ¬_, ← Classical.not_imp]
    by_contra!
    exact h ((this.1 h.nonempty.snd).prod <| this.2 h.nonempty.fst)
  · rintro (h | h)
    · exact h.1.prod_left h.2
    · exact h.1.prod_right h.2

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

Goal state before:
pp: G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a✝ : G
ha : a✝ ∈ S
a : G
s t : Set G
x✝¹ : Fintype ↑s
x✝ : Fintype ↑t
h : ∀ b ∈ s, b * a ∈ t
b : G
hb : b ∈ s
c : G
hc : c ∈ s
hbc :
  (fun x ↦
        match x with
        | ⟨b, hb⟩ => ⟨b * a, ⋯⟩)
      ⟨b, hb⟩ =
    (fun x ↦
        match x with
        | ⟨b, hb⟩ => ⟨b * a, ⋯⟩)
      ⟨c, hc⟩
⊢ ⟨b, hb⟩ = ⟨c, hc⟩

Tactic:
exact Subtype.ext (mul_right_cancel (Subtype.ext_iff.mp hbc))

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

Goal state before:
pp: E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
⊢ IsPretransitive E G

Tactic:
let _ : MulAction E G := MulAction.compHom _ f
  refine ⟨fun x y ↦ ?_⟩
  obtain ⟨m, rfl⟩ : ∃ m : F, m • x = y := exists_smul_eq F x y
  obtain ⟨e, rfl⟩ : ∃ e, f e = m := hf m
  exact ⟨e, rfl⟩

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

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

Tactic:
compl_compl

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (f '' s)ᶜ = (f '' s)ᶜ
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' sᶜ)ᶜ ∪ tᶜᶜ = (f '' sᶜ)ᶜ ∪ t

Tactic:
compl_compl

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' sᶜ)ᶜ ∪ t = (f '' sᶜ)ᶜ ∪ t
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 => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ x = y
Module: Mathlib.Data.Set.Lattice.Image

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

Tactic:
preimage_iInter₂

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
⊢ ⋂ i ∈ s, f ⁻¹' i = ⋂ t ∈ s, f ⁻¹' t
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ {b} * ↑u = {1}

Tactic:
← hb

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
a b : α
ha : ↑u = {a}
hb : ↑u⁻¹ = {b}
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = {1}
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case a.mul
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x hx✝ : M
y : x ∈ closure s
hy✝ : hx✝ ∈ closure s
hx : x = 1 ∨ x ∈ Subsemigroup.closure s
hy : hx✝ = 1 ∨ hx✝ ∈ Subsemigroup.closure s
⊢ x * hx✝ ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy

Goal state after:
case a.mul.inl.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
y : 1 ∈ closure s
hx : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
hy✝ : 1 ∈ closure s
hy : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
⊢ 1 * 1 ∈ {1} ∪ ↑(Subsemigroup.closure s)

case a.mul.inl.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x hx✝ : M
hy✝¹ : hx✝ ∈ closure s
hy✝ : hx✝ = 1 ∨ hx✝ ∈ Subsemigroup.closure s
y : 1 ∈ closure s
hx : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
hy : hx✝ ∈ Subsemigroup.closure s
⊢ 1 * hx✝ ∈ {1} ∪ ↑(Subsemigroup.closure s)

case a.mul.inr.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x : M
y : x ∈ closure s
hx✝ : x = 1 ∨ x ∈ Subsemigroup.closure s
hx : x ∈ Subsemigroup.closure s
hy✝ : 1 ∈ closure s
hy : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
⊢ x * 1 ∈ {1} ∪ ↑(Subsemigroup.closure s)

case a.mul.inr.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x hx✝¹ : M
y : x ∈ closure s
hy✝¹ : hx✝¹ ∈ closure s
hx✝ : x = 1 ∨ x ∈ Subsemigroup.closure s
hy✝ : hx✝¹ = 1 ∨ hx✝¹ ∈ Subsemigroup.closure s
hx : x ∈ Subsemigroup.closure s
hy : hx✝¹ ∈ Subsemigroup.closure s
⊢ x * hx✝¹ ∈ {1} ∪ ↑(Subsemigroup.closure s)
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ map f H = ⊥ ↔ H = ⊥

Tactic:
rw [map_eq_bot_iff, f.ker_eq_bot hf, le_bot_iff]

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
H : (↑e).comp (powMonoidHom n) = (powMonoidHom n).comp ↑e
⊢ Subgroup.map (powMonoidHom n) ⊤ = (powMonoidHom n).range

Tactic:
← range_eq_map

Goal state after:
M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
H : (↑e).comp (powMonoidHom n) = (powMonoidHom n).comp ↑e
⊢ (powMonoidHom n).range = (powMonoidHom n).range
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x : ↥(IsUnit.submonoid M)
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ IsUnit.unit ⋯) x) = x

Tactic:
by simp_rw [IsUnit.unit_spec]

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

Goal state before:
pp: case refine_1
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
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
hx : x ∈ conjugatesOfSet s
⊢ g * x * g⁻¹ ∈ normalClosure s

pp: case refine_2
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
s : Set G
n : G
h : n ∈ normalClosure s
g : G
⊢ g * 1 * g⁻¹ ∈ normalClosure s

pp: case refine_3
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
s : Set G
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * (x * y) * g⁻¹ ∈ normalClosure s

pp: case refine_4
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
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ g * x⁻¹ * g⁻¹ ∈ normalClosure s

Tactic:
· exact conjugatesOfSet_subset_normalClosure (conj_mem_conjugatesOfSet hx)

Goal state after:
case refine_2
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
s : Set G
n : G
h : n ∈ normalClosure s
g : G
⊢ g * 1 * g⁻¹ ∈ normalClosure s

case refine_3
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
s : Set G
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * (x * y) * g⁻¹ ∈ normalClosure s

case refine_4
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
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ g * x⁻¹ * g⁻¹ ∈ normalClosure s
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Tactic:
rintro ⟨a, h, ha⟩
    obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
    exact ⟨x • b, b, ⟨ha, hb⟩, by simp⟩

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l : List ι
f g : ι → M
h : ∀ (i : ι), i ∈ l → g i ≤ f i
⊢ (map g l).prod ≤ (map f l).prod

Tactic:
exact prod_le_prod' h

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

Goal state before:
pp: case left.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
hji : r j✝ i✝
⊢ ⟨i✝, a⟩ = ⟨j✝, b⟩

pp: case left.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hij : r i✝ i✝
hba : s i✝ b a
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩

pp: case right.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hji : r i✝ i✝
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩

pp: case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hba : s i✝ b a
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩

Tactic:
· exact (asymm hij hji).elim

Goal state after:
case left.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hij : r i✝ i✝
hba : s i✝ b a
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩

case right.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hji : r i✝ i✝
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩

case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hba : s i✝ b a
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩
Module: Mathlib.Algebra.Group.Submonoid.Membership

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

Tactic:
exact .inr rfl

Goal state after:
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, a✝}

Tactic:
exact .inr rfl

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

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

Tactic:
exact .inr rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ ∀ {a_1 b : M}, a_1 ∈ {1, a} → b ∈ {1, a} → a_1 * b ∈ {1, a}

Tactic:
rintro _ _ (rfl | rfl) (rfl | rfl)
      · rw [one_mul]; exact .inl rfl
      · rw [one_mul]; exact .inr rfl
      · rw [mul_one]; exact .inr rfl
      · rw [ha]; exact .inr rfl

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
⊢ ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m

Tactic:
induction l using List.reverseRecOn with
  | nil => simp
  | append_singleton tl a ih => ?_
  intro b m o hb ho
  rw [foldl_append, foldl_cons, foldl_nil, argAux] at ho
  rcases hf : foldl (argAux r) o tl with - | c
  · rw [hf] at ho
    rw [foldl_argAux_eq_none] at hf
    simp_all [hf.1, hf.2, hr₀.irrefl _]
  rw [hf, Option.mem_def] at ho
  grind +splitIndPred

Goal state after: