mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
⊢ ∃ i, (∃ a b, a ∈ image (fun x ↦ x i) s ∧ b ∈ image (fun x ↦ x i) s ∧ a ≠ b) ∧ ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s

Tactic:
refine ⟨i, ⟨_, _, mem_image_of_mem _ h1, mem_image_of_mem _ h2, hne⟩, fun ai => ?_⟩

Goal state after:
ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
ai : α i
⊢ {x ∈ s | x i = ai} ⊂ s
Module: Mathlib.Data.Fin.SuccPred

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

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

Tactic:
· rw [predAbove_of_castSucc_lt _ _ h, predAbove_succ_of_le _ _ h, succ_pred]

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

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 3 → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

pp: case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → #s = 3

Tactic:
· rw [card_eq_succ]
    grind [card_eq_two]

Goal state after:
case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → #s = 3
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
cases nonempty_fintype α
  obtain ⟨l, e⟩ := Quotient.exists_rep (@univ α _).1
  have := And.intro (@univ α _).2 (@mem_univ_val α _)
  exact ⟨_, by rwa [← e] at this⟩

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

Goal state before:
pp: case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ append x₀ x (castAdd n i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n i)

Tactic:
Subsingleton.elim i 0,

Goal state after:
case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ append x₀ x (castAdd n 0) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n 0)
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:
Subsingleton.elim i 0,

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

Goal state before:
pp: case cast.last
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i : Fin n
h : snoc x x₀ i.castSucc = snoc x x₀ (last n)
⊢ i.castSucc = last n

Tactic:
simp only [snoc_castSucc, snoc_last] at h
      rw [← h] at hx₀
      apply hx₀.elim (Set.mem_range_self i)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
i : Infinite ι
s : Finset ι
w : #s ≤ n
c : #s = n + 1
⊢ False

Tactic:
rw [c] at w

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
i : Infinite ι
s : Finset ι
w : n + 1 ≤ n
c : #s = n + 1
⊢ False
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
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₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
⊢ ∀ (H₂ : i.succAbove ((i.succAbove j).pred H₁) = i.succAbove j), H₂ ▸ p ((i.succAbove j).pred H₁) = p j

Tactic:
generalize hk : pred (succAbove i j) H₁ = k

Goal state after:
case neg
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₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
k : Fin n
hk : (i.succAbove j).pred H₁ = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : j < i
x : α i
p : (k : Fin n) → α (i.succAbove k)
⊢ (if hj : j = i then ⋯ ▸ x else if hlt : j < i then ⋯ ▸ p (j.castPred ⋯) else ⋯ ▸ p (j.pred ⋯)) = ⋯ ▸ p (j.castPred ⋯)

Tactic:
dif_neg (Fin.ne_of_lt h),

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : j < i
x : α i
p : (k : Fin n) → α (i.succAbove k)
⊢ (if hlt : j < i then ⋯ ▸ p (j.castPred ⋯) else ⋯ ▸ p (j.pred ⋯)) = ⋯ ▸ p (j.castPred ⋯)
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)
j : Fin n
⊢ snoc (fun j ↦ cast ⋯ (p j)) x j.castSucc ≍ (last n).removeNth (snoc (fun j ↦ cast ⋯ (p j)) x) j

Tactic:
apply congr_arg_heq
    rw [succAbove_last]

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
s : Finset α
a : α
ha : a ∉ s
⊢ ∃ s_1, #s_1 = #s + 1

Tactic:
exact ⟨insert a s, card_insert_of_notMem ha⟩

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ IsChain r (range n.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
isChain_range,

Goal state after:
r : ℕ → ℕ → Prop
n : ℕ
⊢ (∀ (m : ℕ), m < n.succ - 1 → r m m.succ) ↔ ∀ (m : ℕ), m < n → r m m.succ
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : ¬a ∈ as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum

Tactic:
simp only [dedup_cons_of_notMem ha, List.filter]

Goal state after:
case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : ¬a ∈ as
⊢ (map (fun i ↦ count i as)
        (match p a with
        | true => a :: filter p as.dedup
        | false => filter p as.dedup)).sum =
    (map (fun i ↦ count i as) (filter p as.dedup)).sum
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l hl, IsChain r l ∧ l.head hl = a ∧ l.getLast hl = b

Tactic:
by
  rcases exists_isChain_cons_of_relationReflTransGen h with ⟨l, _⟩; grind

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

Goal state before:
pp: α : Type u_1
s : Multiset α
n : ℕ
a : α
⊢ n • ({a} + s) = n • {a} + n • s

Tactic:
nsmul_add

Goal state after:
α : Type u_1
s : Multiset α
n : ℕ
a : α
⊢ n • {a} + n • s = n • {a} + n • s
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • {a}) + n • filter p ha = n • ((if p a then {a} else 0) + filter p ha)

Tactic:
nsmul_add

Goal state after:
case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • {a}) + n • filter p ha = (n • if p a then {a} else 0) + n • filter p ha
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ (l.rotate n)[0]? = l[n]?

Tactic:
getElem?_rotate (n.zero_le.trans_lt h),

Goal state after:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ l[(0 + n) % l.length]? = l[n]?
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
h : Rel (Rel r) s t
⊢ Rel r s.join t.join

Tactic:
by
  induction h with
  | zero => simp
  | cons hab hst ih => simpa using hab.add ih

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

Goal state before:
pp: i j : ℕ
⊢ i ! * j ! ∣ (i + j)!

Tactic:
suffices i ! * (i + j - i)! ∣ (i + j)! by
    rwa [Nat.add_sub_cancel_left i j] at this
  exact factorial_mul_factorial_dvd_factorial (Nat.le_add_right _ _)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
a : α
⊢ ∀ (a' : α) (m : Multiset α) (b : Multiset ((a : α) → a ∈ m → β a)),
    ((t a).bind fun b_1 ↦ map (Pi.cons (a' ::ₘ m) a b_1) ((t a').bind fun b_2 ↦ map (Pi.cons m a' b_2) b)) ≍
      (t a').bind fun b_1 ↦ map (Pi.cons (a ::ₘ m) a' b_1) ((t a).bind fun b_2 ↦ map (Pi.cons m a b_2) b)

Tactic:
a'

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
⊢ ∀ (m : Multiset α) (b : Multiset ((a : α) → a ∈ m → β a)),
    ((t a).bind fun b_1 ↦ map (Pi.cons (a' ::ₘ m) a b_1) ((t a').bind fun b_2 ↦ map (Pi.cons m a' b_2) b)) ≍
      (t a').bind fun b_1 ↦ map (Pi.cons (a ::ₘ m) a' b_1) ((t a).bind fun b_2 ↦ map (Pi.cons m a b_2) b)
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: ι : Type u_2
π : ι → Type u_3
s t : Finset ι
inst✝ : DecidablePred fun x ↦ x ∈ s
hst : s ⊆ t
u : (i : ↥s) → Set (π ↑i)
⊢ restrict₂ hst ⁻¹' Set.univ.pi u = Set.univ.pi fun j ↦ if h : ↑j ∈ s then u ⟨↑j, h⟩ else Set.univ

Tactic:
grind [restrict₂]

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

Goal state before:
pp: case inr
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
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
⊢ ∀ b ∈ S ^ (n + 2), b * a⁻¹ ∈ S ^ (n + 1)

Tactic:
replace h₂ : S ^ n * {a} = S ^ (n + 1) := by
    have : Fintype (S ^ n * Set.singleton a) := by
      classical
      apply fintypeMul
    refine Set.eq_of_subset_of_card_le ?_ (le_trans (ge_of_eq h) ?_)
    · exact mul_subset_mul Set.Subset.rfl (Set.singleton_subset_iff.mpr ha)
    · convert! key a (S ^ n) (S ^ n * { a }) fun b hb ↦ Set.mul_mem_mul hb (Set.mem_singleton a)

Goal state after:
case inr
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
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : S ^ n * {a} = S ^ (n + 1)
⊢ ∀ b ∈ S ^ (n + 2), b * a⁻¹ ∈ S ^ (n + 1)
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
⊢ a ∈ (ConjClasses.mk b).carrier ↔ ConjClasses.mk a = ConjClasses.mk b

Tactic:
rw [carrier, eq_comm, mk_eq_mk_iff_isConj, ← quotient_mk_eq_mk, Quotient.lift_mk]

Goal state after:
α : Type u
inst✝ : Monoid α
a b : α
⊢ a ∈ conjugatesOf b ↔ IsConj b a
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
carrier : Set M
mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
⊢ { carrier := carrier, mul_mem' := mul_mem' } = ⊤ ↔ carrier = Set.univ

Tactic:
simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
carrier : Set M
mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
⊢ { carrier := carrier, mul_mem' := mul_mem' } = ⊥ ↔ carrier = ∅

Tactic:
simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
toSubsemigroup : Subsemigroup M
one_mem' : 1 ∈ toSubsemigroup.carrier
⊢ { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' } = ⊤ ↔ toSubsemigroup = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
toSubsemigroup : Subsemigroup M
one_mem' : 1 ∈ toSubsemigroup.carrier
⊢ { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' } = ⊥ ↔ ↑toSubsemigroup = {1}

Tactic:
simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
y : β
hy : y ∈ t
⊢ y ∈ f '' ⋂ i, s i

Tactic:
rw [Hinj.image_iInter_eq, mem_iInter]

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
y : β
hy : y ∈ t
⊢ ∀ (i : ι), y ∈ f '' s i
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂ r, ⋂ i, ⋂ (_ : i ∈ S ∧ (i, t) = r), r.1 ×ˢ r.2 = ⋂ s ∈ S, s ×ˢ t

Tactic:
biInter_and',

Goal state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂ y ∈ S, ⋂ x, ⋂ (_ : (y, t) = x), x.1 ×ˢ x.2 = ⋂ s ∈ S, s ×ˢ t
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_1.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ s = {a}

Tactic:
refine eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩

Goal state after:
case refine_1.refine_1
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ s
⊢ x = a
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
⊢ t = {b}

Tactic:
refine eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩

Goal state after:
case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂ r, ⋂ i, ⋂ (_ : i ∈ T ∧ (s, i) = r), r.1 ×ˢ r.2 = ⋂ t ∈ T, s ×ˢ t

Tactic:
biInter_and',

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
n : ℤ
s t : Set α
h : s * t = 1
⊢ s⁻¹ = t

Tactic:
obtain ⟨a, b, rfl, rfl, hab⟩ := Set.mul_eq_one_iff.1 h

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s t : Set α
n : ℤ
a b : α
hab : a * b = 1
h : {a} * {b} = 1
⊢ {a}⁻¹ = {b}
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} ∪ ↑(Subsemigroup.closure s)
hy : hx✝ ∈ {1} ∪ ↑(Subsemigroup.closure s)
⊢ x * hx✝ ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
push _ ∈ _ at hx hy

Goal state after:
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)
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
q : Subgroup G
hp : Set G
mul_mem'✝ : ∀ {a b : G}, a ∈ hp → b ∈ hp → a * b ∈ hp
one_mem'✝ : 1 ∈ { carrier := hp, mul_mem' := mul_mem'✝ }.carrier
inv_mem'✝ :
  ∀ {x : G},
    x ∈ { carrier := hp, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
      x⁻¹ ∈ { carrier := hp, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
h :
  (fun s ↦ s.carrier) { carrier := hp, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, inv_mem' := inv_mem'✝ } =
    (fun s ↦ s.carrier) q
⊢ { carrier := hp, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, inv_mem' := inv_mem'✝ } = q

Tactic:
obtain ⟨⟨⟨hq, _⟩, _⟩, _⟩ := q

Goal state after:
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
hp : Set G
mul_mem'✝¹ : ∀ {a b : G}, a ∈ hp → b ∈ hp → a * b ∈ hp
one_mem'✝¹ : 1 ∈ { carrier := hp, mul_mem' := mul_mem'✝¹ }.carrier
inv_mem'✝¹ :
  ∀ {x : G},
    x ∈ { carrier := hp, mul_mem' := mul_mem'✝¹, one_mem' := one_mem'✝¹ }.carrier →
      x⁻¹ ∈ { carrier := hp, mul_mem' := mul_mem'✝¹, one_mem' := one_mem'✝¹ }.carrier
hq : Set G
mul_mem'✝ : ∀ {a b : G}, a ∈ hq → b ∈ hq → a * b ∈ hq
one_mem'✝ : 1 ∈ { carrier := hq, mul_mem' := mul_mem'✝ }.carrier
inv_mem'✝ :
  ∀ {x : G},
    x ∈ { carrier := hq, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier →
      x⁻¹ ∈ { carrier := hq, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝ }.carrier
h :
  (fun s ↦ s.carrier) { carrier := hp, mul_mem' := mul_mem'✝¹, one_mem' := one_mem'✝¹, inv_mem' := inv_mem'✝¹ } =
    (fun s ↦ s.carrier) { carrier := hq, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, inv_mem' := inv_mem'✝ }
⊢ { carrier := hp, mul_mem' := mul_mem'✝¹, one_mem' := one_mem'✝¹, inv_mem' := inv_mem'✝¹ } =
    { carrier := hq, mul_mem' := mul_mem'✝, one_mem' := one_mem'✝, inv_mem' := inv_mem'✝ }
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
A : Type u_4
inst✝² : AddGroup A
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
K : Subgroup G
f : G →* N
g : N →* G
h : LeftInverse ⇑g ⇑f
⊢ RightInverse (⇑g ∘ ⇑f.range.subtype) ⇑f.rangeRestrict

Tactic:
by
      rintro ⟨x, y, rfl⟩
      solve_by_elim

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
N : Type u_5
P : Type u_6
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x : G
hx : x ∈ f.ker
y : G
⊢ y * x * y⁻¹ ∈ f.ker

Tactic:
rw [mem_ker, map_mul, map_mul, mem_ker.1 hx, mul_one, map_mul_eq_one f (mul_inv_cancel y)]

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: m n : ℕ
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + (max m n + 1))

Tactic:
split_ifs <;> simp [Nat.le_of_lt, not_lt.1, *] <;> lia

Goal state after:
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
H K✝ : Subgroup G
inst✝ : H.Characteristic
K : Subgroup ↥H
hK : K.Characteristic
φ : G ≃* G
⊢ map φ.toMonoidHom (map H.subtype K) = map H.subtype K

Tactic:
have := congr_arg (map H.subtype) <| characteristic_iff_map_eq.1 hK (MulAut.characteristic H φ)

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
H K✝ : Subgroup G
inst✝ : H.Characteristic
K : Subgroup ↥H
hK : K.Characteristic
φ : G ≃* G
this : map H.subtype (map (MulEquiv.toMonoidHom ((MulAut.characteristic H) φ)) K) = map H.subtype K
⊢ map φ.toMonoidHom (map H.subtype K) = map H.subtype K
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 ∈ H

Tactic:
by
  rw [← mul_one a, ← inv_one, ← one_mul a]
  exact h 1

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
h : Forall₂ (fun x1 x2 ↦ x1 ≤ x2) l₁ l₂
⊢ l₁.prod ≤ l₂.prod

Tactic:
induction h with
  | nil => rfl
  | cons hab ih ih' => simpa only [prod_cons] using mul_le_mul' hab ih'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LE β
x y : α × β
⊢ toLex y ≤ toLex x ↔ y.1 < x.1 ∨ x.1 = y.1 ∧ y.2 ≤ x.2

Tactic:
rw [eq_comm, toLex_le_toLex]

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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : a₁ < a₂
c : α
h₁ : a₁ < c
h₂ : c < a₂
⊢ ∃ a, (a₁, b₁) < a ∧ a < (a₂, b₂)

Tactic:
exact ⟨(c, b₁), left _ _ h₁, left _ _ h₂⟩

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
S : Submonoid M
inst✝ : Fintype ↥S
h : card ↥S ≤ 1
x : M
hx : x ∈ S
⊢ x = 1

Tactic:
simpa [Subtype.ext_iff] using card_le_one_iff.1 h ⟨x, hx⟩ 1

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
h : 0 < l.length
⊢ maximum_of_length_pos h ∈ l

Tactic:
apply maximum_mem

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
l : List α
h : 0 < l.length
⊢ l.maximum = ↑(maximum_of_length_pos h)
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (↑(insert a s)) (max a (s.max' H))

Tactic:
rw [coe_insert]
    exact (isGreatest_max' _ _).insert _

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
s : Finset ι
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
⊢ motive s

Tactic:
by
  induction s using Finset.eraseInduction with | _ s ihs
  rcases (s.image f).eq_empty_or_nonempty with (hne | hne)
  · simp only [image_eq_empty] at hne
    simp only [hne, empty]
  · have H : (s.image f).max' hne ∈ s.image f := max'_mem (s.image f) hne
    simp only [mem_image] at H
    rcases H with ⟨a, has, hfa⟩
    rw [← insert_erase has]
    refine insert _ _ (notMem_erase a s) (fun x hx => ?_) (ihs a has)
    rw [hfa]
    exact le_max' _ _ (mem_image_of_mem _ <| mem_of_mem_erase hx)

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

Goal state before:
pp: case nil
α : Type u
l₁ l₂ : List α
h : (l₁, l₂) ∈ [].sublists'.zip [].sublists'.reverse
⊢ l₁ ++ l₂ ~ []

Tactic:
simp_all only [sublists'_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons,
      zip_nil_right, mem_singleton, Prod.mk.injEq, append_nil, Perm.refl]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ (insert a s).powerset = s.powerset ∪ image (insert a) s.powerset

Tactic:
ext t
  simp only [mem_powerset, mem_image, mem_union, subset_insert_iff]
  grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ (↑s.powerset).PairwiseDisjoint fun t ↦ {t, insert a t}

Tactic:
simp_rw [Set.pairwiseDisjoint_iff, mem_coe, mem_powerset]

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ ∀ ⦃i : Finset α⦄, i ⊆ s → ∀ ⦃j : Finset α⦄, j ⊆ s → ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ (↑s.powerset).PairwiseDisjoint fun t ↦ {t, insert a t}

Tactic:
by
  simp_rw [Set.pairwiseDisjoint_iff, mem_coe, mem_powerset]
  rintro i hi j hj
  simp only [Set.Nonempty, Set.mem_inter_iff, Set.mem_insert_iff, Set.mem_singleton_iff,
    exists_eq_or_imp, exists_eq_left, or_imp, imp_self, true_and]
  refine ⟨?_, ?_, insert_erase_invOn.2.injOn (notMem_mono hi ha) (notMem_mono hj ha)⟩ <;>
    rintro rfl <;>
    cases Finset.notMem_mono ‹_› ha (Finset.mem_insert_self _ _)

Goal state after: