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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁⁻¹ * v₂ = p₁ /ₛ p₂ ↔ v₂ / v₁ = p₁ /ₛ p₂

Tactic:
inv_mul_eq_div

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₂ / v₁ = p₁ /ₛ p₂ ↔ v₂ / v₁ = p₁ /ₛ p₂
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mpr
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
h : a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs

Tactic:
rcases h with (⟨eq₁, eq₂⟩ | ⟨_, cs, eq₁, eq₂⟩)

Goal state after:
case mpr.inl
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq₁ : a = b
eq₂ : as = bs
⊢ a ::ₘ as = b ::ₘ bs

case mpr.inr
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
left✝ : a ≠ b
cs : Multiset α
eq₁ : as = b ::ₘ cs
eq₂ : bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs
Module: Mathlib.Data.Set.List

Goal state before:
pp: α : Type u_1
inst✝ : Inhabited α
l : List α
⊢ range l.getI = insert default {x | x ∈ l}

Tactic:
unfold List.getI
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t - t = s

Tactic:
by ext a; simp

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ map f s = 0 ↔ s = 0

Tactic:
rw [← Multiset.card_eq_zero, Multiset.card_map, Multiset.card_eq_zero]

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 ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂

Tactic:
hl₁.sdiff_eq_filter,

Goal state after:
α : 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₂
Module: Mathlib.Data.List.Nodup

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

Tactic:
decide_eq_true_iff

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
this : b ∈ map f s
⊢ ∃ a, a ∈ s ∧ f a = b ∧ map f (s.erase a) = t

Tactic:
obtain ⟨a, h1, rfl⟩ := mem_map.mp this

Goal state after:
case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
a : α
h1 : a ∈ s
h : map f s = f a ::ₘ t
this : f a ∈ map f s
⊢ ∃ a_1, a_1 ∈ s ∧ f a_1 = f a ∧ map f (s.erase a_1) = t
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s = map f t ↔ s = t

Tactic:
rw [← rel_eq, ← rel_eq, rel_map]

Goal state after:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ Rel (fun a b ↦ f a = f b) s t ↔ Rel (fun x1 x2 ↦ x1 = x2) s t
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ map (fun x ↦ f ↑x) s.attach = map g (map (fun x ↦ i ↑x ⋯) s.attach)

Tactic:
Multiset.map_map

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ map (fun x ↦ f ↑x) s.attach = map (g ∘ fun x ↦ i ↑x ⋯) s.attach
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a s = count a s - count a t + min (count a s) (count a t)

Tactic:
Nat.sub_add_min_cancel

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a s = count a s
Module: Mathlib.Data.Finset.Dedup

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

Tactic:
by
  simp_rw [Finset.ssubset_def, toFinset_subset]
  rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
m1 m2 : Multiset α
⊢ Disjoint m1.toFinset m2.toFinset ↔ Disjoint m1 m2

Tactic:
by
  simp [disjoint_left, Finset.disjoint_left]

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.13
β : α → Type u_4
inst✝¹ : (a : α) → DecidableEq (β a)
inst✝ : Fintype α
f g : (a : α) → β a
⊢ (∀ (a : α), a ∈ univ → f a = g a) ↔ f = g

Tactic:
by simp [funext_iff]

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

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ (piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = f ⟨i, hi⟩

Tactic:
piFinsetUnion,

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ ((sumPiEquivProdPi fun b ↦ α ↑((Finset.union s t h) b)).symm.trans (piCongrLeft (fun i ↦ α ↑i) (Finset.union s t h)))
      (f, g) ⟨i, hi'⟩ =
    f ⟨i, hi⟩
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ univ ∩ s = s

Tactic:
by ext a; simp

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

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ (piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = g ⟨i, hi⟩

Tactic:
piFinsetUnion,

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ ((sumPiEquivProdPi fun b ↦ α ↑((Finset.union s t h) b)).symm.trans (piCongrLeft (fun i ↦ α ↑i) (Finset.union s t h)))
      (f, g) ⟨i, hi'⟩ =
    g ⟨i, hi⟩
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ (fun p ↦ p.predAbove i) a ≤ (fun p ↦ p.predAbove i) b

Tactic:
dsimp [predAbove]
  split_ifs with ha hb hb
  · rfl
  · exact pred_le _
  · have : b < a := castSucc_lt_castSucc_iff.mpr (hb.trans_le (le_of_not_gt ha))
    exact absurd H this.not_ge
  · rfl

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

Goal state before:
pp: n m : ℕ
eq : n = m
a b : Fin n
⊢ Fin.cast eq a = Fin.cast eq b ↔ a = b

Tactic:
by
  simp [← val_inj]

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

Goal state before:
pp: case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
grind [castSucc_ne_zero_iff]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ (last n).succAbove i = i.castSucc

Tactic:
succAbove_last

Goal state after:
n : ℕ
i : Fin n
⊢ i.castSucc = i.castSucc
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ (g ∘ cons y q) j'.succ = cons (g y) (g ∘ q) j'.succ

Tactic:
cons_succ,

Goal state after:
case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ (g ∘ cons y q) j'.succ = (g ∘ q) j'
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case cons_mem
α : Type u_1
l : List α
x : α
l✝ : List α
a✝ : x ∈ l✝
⊢ x ∈ x :: l✝

Tactic:
| cons_mem =>

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

Goal state before:
pp: α : Sort u_4
β : Sort u_5
inst✝ : Finite β
f : α → β
H : Injective f
n : ℕ
e : β ≃ Fin n
⊢ Finite α

Tactic:
exact .of_equiv (Set.range (e ∘ f)) (Equiv.ofInjective _ (e.injective.comp H)).symm

Goal state after:
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)
⊢ i.insertNth x p j = ⋯ ▸ p (j.castPred ⋯)

Tactic:
insertNth,

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)
⊢ i.succAboveCases x p j = ⋯ ▸ p (j.castPred ⋯)
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
insertNth,

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : i < j
x : α i
p : (k : Fin n) → α (i.succAbove k)
⊢ i.succAboveCases x p j = ⋯ ▸ p (j.pred ⋯)
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
⊢ j.castSucc = (last n).succAbove j

Tactic:
succAbove_last

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b : α
l : List α
⊢ List.foldl (fun x y ↦ op y x) b l = List.foldl op b l

Tactic:
by simp [hc.comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x ↦ m (f x)) s.val) =
    Multiset.fold op' (m b) (Multiset.map m (Multiset.map f s.val))

Tactic:
Multiset.map_map

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x ↦ m (f x)) s.val) = Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ (find? fun x ↦ decide (p x)) = if h : ∃ i, p i then some (Fin.find p h) else none

Tactic:
find?_eq_dite,

Goal state after:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ (if h : ∃ i, decide (p i) = true then some (Fin.find (fun x ↦ decide (p x) = true) h) else none) =
    if h : ∃ i, p i then some (Fin.find p h) else none
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
i : Fin n
p : Fin n → Bool
h : p i = true
⊢ (find? p).get ⋯ = Fin.find (fun x ↦ p x = true) ⋯

Tactic:
find?_eq_dite,

Goal state after:
n : ℕ
i : Fin n
p : Fin n → Bool
h : p i = true
⊢ (if h : ∃ i, p i = true then some (Fin.find (fun x ↦ p x = true) h) else none).get ⋯ = Fin.find (fun x ↦ p x = true) ⋯
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Bool
h : ∃ i, p i = true
⊢ find? p = some (Fin.find (fun x ↦ p x = true) h)

Tactic:
find?_eq_dite,

Goal state after:
n : ℕ
p : Fin n → Bool
h : ∃ i, p i = true
⊢ (if h : ∃ i, p i = true then some (Fin.find (fun x ↦ p x = true) h) else none) =
    some (Fin.find (fun x ↦ p x = true) h)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Bool
h : (find? p).isSome = true
⊢ find? p = some (Fin.find (fun x ↦ p x = true) ⋯)

Tactic:
find?_eq_dite,

Goal state after:
n : ℕ
p : Fin n → Bool
h : (find? p).isSome = true
⊢ (if h : ∃ i, p i = true then some (Fin.find (fun x ↦ p x = true) h) else none) =
    some (Fin.find (fun x ↦ p x = true) ⋯)
Module: Mathlib.Data.List.Range

Goal state before:
pp: r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (IsChain r (0 :: map succ (range n)) ↔ IsChain r (0 :: map succ (range n)))

Tactic:
exact fun _ => Iff.rfl

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
x y : α
⊢ IsChain R [x, y] ↔ R x y

Tactic:
by
  simp only [IsChain.singleton, isChain_cons_cons, and_true]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a b : α
⊢ IsChain R (a :: l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])

Tactic:
isChain_iff_forall₂,

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a b : α
⊢ Forall₂ R (a :: l ++ [b]).dropLast (a :: l ++ [b]).tail ↔ Forall₂ R (a :: l) (l ++ [b])
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons
α : 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
⊢ (map (fun x ↦ count x (a :: as)) (filter p (a :: as).dedup)).sum = countP p (a :: as)

Tactic:
List.countP_cons,

Goal state after:
case cons
α : 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
⊢ (map (fun x ↦ count x (a :: as)) (filter p (a :: as).dedup)).sum = countP p as + if p a = true then 1 else 0
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 ::ₘ ha)) = n • filter p (a ::ₘ ha)

Tactic:
nsmul_cons,

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 • ha) = n • filter p (a ::ₘ ha)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ l.alternatingProd ^ (-1) ^ (l.length + 1) * [a].alternatingProd ^ (-1) ^ l.reverse.length =
    (a :: l).alternatingProd ^ (-1) ^ ((a :: l).length + 1)

Tactic:
alternatingProd_singleton,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ l.alternatingProd ^ (-1) ^ (l.length + 1) * a ^ (-1) ^ l.reverse.length =
    (a :: l).alternatingProd ^ (-1) ^ ((a :: l).length + 1)
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst✝ : DecidableEq α
⊢ s.pi t = ∅ ↔ ∃ a ∈ s, t a = ∅

Tactic:
contrapose!; exact pi_nonempty

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s.offDiag = #s * #s - #s

Tactic:
← sq

Goal state after:
α : Type u_1
s : Finset α
⊢ #s.offDiag = #s ^ 2 - #s
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ n.choose (k + 1) * (n + 1) = 0 * (n + 1 - (k + 1))

Tactic:
choose_eq_zero_of_lt (n.lt_succ_self.trans hk),

Goal state after:
case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ 0 * (n + 1) = 0 * (n + 1 - (k + 1))
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ t) = t

Tactic:
by
  obtain rfl | ht := t.eq_empty_or_nonempty
  · have : Nonempty α := ⟨a⟩
    simp
  · exact eval_image_piFinset (fun _ ↦ t) a fun _ _ ↦ ht

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

Goal state before:
pp: M✝ : Type u_1
G : Type u_2
α✝ : Type u_3
β : Type u_4
M : Type u_5
α : Type u_6
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Subsingleton α
x y : α
⊢ 1 • x = y

Tactic:
simp only [one_smul, Subsingleton.elim x y]

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
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Tactic:
by
  have hG : 0 < Fintype.card G := Fintype.card_pos
  rcases S.eq_empty_or_nonempty with (rfl | ⟨a, ha⟩)
  · refine fun k hk ↦ Fintype.card_congr ?_
    rw [empty_pow (hG.trans_le hk).ne', empty_pow (ne_of_gt hG)]
  have key : ∀ (a) (s t : Set G) [Fintype s] [Fintype t],
      (∀ b : G, b ∈ s → b * a ∈ t) → Fintype.card s ≤ Fintype.card t := by
    refine fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨b * a, h b hb⟩) ?_
    rintro ⟨b, hb⟩ ⟨c, hc⟩ hbc
    exact Subtype.ext (mul_right_cancel (Subtype.ext_iff.mp hbc))
  have mono : Monotone (fun n ↦ Fintype.card (↥(S ^ n)) : ℕ → ℕ) :=
    monotone_nat_of_le_succ fun n ↦ key a _ _ fun b hb ↦ Set.mul_mem_mul hb ha
  refine fun _ ↦ Nat.stabilises_of_monotone mono (fun n ↦ set_fintype_card_le_univ (S ^ n))
    fun n h ↦ le_antisymm (mono (n + 1).le_succ) (key a⁻¹ (S ^ (n + 2)) (S ^ (n + 1)) ?_)
  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)
  rw [pow_succ', ← h₂, ← mul_assoc, ← pow_succ', h₂, mul_singleton, forall_mem_image]
  intro x hx
  rwa [mul_inv_cancel_right]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ f ↑c * f a = f b * f ↑c

Tactic:
← f.map_mul,

Goal state after:
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ f (↑c * a) = f b * f ↑c
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s✝ : Set M
S : Subsemigroup M
p : M → Prop
s : Set M
closure : Subsemigroup.closure s = ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
⊢ p x

Tactic:
by
  induction x using dense_induction s with
  | closure => exact closure
  | mem x hx => exact mem x hx
  | mul _ _ h₁ h₂ => exact mul _ _ h₁ h₂

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
p : α → Prop
⊢ (∀ (x : α), x⁻¹ ∈ s → p x) ↔ ∀ (x : α), x ∈ s → p x⁻¹

Tactic:
by
  rw [← (Equiv.inv _).forall_congr_right]
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
T : Set (Set β)
hS : S.Nonempty
hT : T.Nonempty
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2

Tactic:
obtain ⟨s₁, h₁⟩ := hS
  obtain ⟨s₂, h₂⟩ := hT
  refine Set.Subset.antisymm (sInter_prod_sInter_subset S T) fun x hx => ?_
  rw [mem_iInter₂] at hx
  exact ⟨fun s₀ h₀ => (hx (s₀, s₂) ⟨h₀, h₂⟩).1, fun s₀ h₀ => (hx (s₁, s₀) ⟨h₁, h₀⟩).2⟩

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s

Tactic:
rintro ⟨a, rfl, ha⟩

Goal state after:
case mpr
α : Type u_2
inst✝ : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit {a}
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set β
⊢ (⇑f ⁻¹' s) ^ 0 ⊆ ⇑f ⁻¹' s ^ 0

Tactic:
by simp [Set.subset_def]

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
ι : Sort u_7
inst✝ : Nonempty ι
f : G →* N
hf : Injective ⇑f
s : ι → Subgroup G
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Goal state after:
G : Type u_1
inst✝² : Group G
N : Type u_5
inst✝¹ : Group N
ι : Sort u_7
inst✝ : Nonempty ι
f : G →* N
hf : Injective ⇑f
s : ι → Subgroup G
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ A ⊔ A' = B ⊓ A ⊔ B ⊓ A'

Tactic:
inf_of_le_right hA',

Goal state after:
G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ A ⊔ A' = B ⊓ A ⊔ A'
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
F : Type u_4
inst✝¹ : FunLike F M N
mc : MonoidHomClass F M N
ι : Sort u_5
inst✝ : Nonempty ι
f : F
hf : Injective ⇑f
s : ι → Submonoid M
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
F : Type u_4
inst✝¹ : FunLike F M N
mc : MonoidHomClass F M N
ι : Sort u_5
inst✝ : Nonempty ι
f : F
hf : Injective ⇑f
s : ι → Submonoid M
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))
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
g : N →* P
f : M →* N
⊢ map g (mrange f) = mrange (g.comp f)

Tactic:
by
  simpa only [mrange_eq_map] using (⊤ : Submonoid M).map_map g f

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

Goal state before:
pp: case pos
m n : ℕ
h✝ : m < n
⊢ n * n + m < max m n * max m n + (max m n + (max m n + 1))

Tactic:
simp [Nat.le_of_lt, not_lt.1, *]

Goal state after:
case pos
m n : ℕ
h✝ : m < n
⊢ m < n + (n + 1)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case neg
m n : ℕ
h✝ : ¬m < n
⊢ m * m + (m + n) < max m n * max m n + (max m n + (max m n + 1))

Tactic:
simp [Nat.le_of_lt, not_lt.1, *]

Goal state after:
case neg
m n : ℕ
h✝ : ¬m < n
⊢ n < m + 1
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: m n : ℕ
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n

Tactic:
rcases lt_or_ge m n with h | h

Goal state after:
case inl
m n : ℕ
h : m < n
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n

case inr
m n : ℕ
h : n ≤ m
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
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
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * (b * a * (b⁻¹ * c⁻¹)) ∈ H

Tactic:
← mul_inv_rev,

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
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * (b * a * (c * b)⁻¹) ∈ H
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'
⊢ (f.prodMap g).ker = f.ker.prod g.ker

Tactic:
← comap_bot,

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) ⊥ = f.ker.prod g.ker
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) ⊥ = f.ker.prod g.ker

Tactic:
← comap_bot,

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 ⊥).prod g.ker