mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
h₁ : a'' ≠ a
b' : δ a''
h : a ≠ a''
ha₁ : a'' ∈ a ::ₘ a'' ::ₘ m
ha₂ : a'' ∈ a'' ::ₘ a ::ₘ m
x✝ : ha₁ ≍ ha₂
⊢ cons (a'' ::ₘ m) a b (cons m a'' b' f) a'' ha₁ ≍ cons (a ::ₘ m) a'' b' (cons m a b f) a'' ha₂

Tactic:
simp [*, Pi.cons_same, Pi.cons_ne]

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

Goal state before:
pp: case inl.inr
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
ha₁ : a'' ∈ a ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a ::ₘ m
x✝ : ha₁ ≍ ha₂
h₁ : a'' ≠ a
h₂ : a'' ≠ a'
⊢ cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁ ≍ cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂

Tactic:
simp [*, Pi.cons_same, Pi.cons_ne]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a' : α
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
a'' : α
b : δ a''
h : a'' ≠ a'
ha₁ : a'' ∈ a'' ::ₘ a' ::ₘ m
ha₂ : a'' ∈ a' ::ₘ a'' ::ₘ m
x✝ : ha₁ ≍ ha₂
⊢ cons (a' ::ₘ m) a'' b (cons m a' b' f) a'' ha₁ ≍ cons (a'' ::ₘ m) a' b' (cons m a'' b f) a'' ha₂

Tactic:
simp [*, Pi.cons_same, Pi.cons_ne]

Goal state after:
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
hf : DependsOn f ∅
x y : (i : ι) → α i
⊢ ∀ i ∈ ∅, x i = y i

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) + #({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})

Tactic:
← card_union_of_disjoint

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})

α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ ↑(s ∪ t).offDiag = ↑(s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s)

Tactic:
by
    push_cast
    exact Set.offDiag_union (disjoint_coe.2 h)

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : Nonempty α
⊢ (piFinset fun x ↦ ∅) = ∅

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
γ : α → Type u_3
inst✝ : IsEmpty α
s : (a : α) → Finset (γ a)
x✝ : (a : α) → γ a
⊢ x✝ ∈ piFinset s

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ (fun b ↦ if h : a = b then h ▸ x else f b h) a = x

Tactic:
by simp

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)
⊢ (pi 0 t).card = (map (fun a ↦ (t a).card) 0).prod

Tactic:
by simp

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : α → Type u_4
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
⊢ ∀ (x : (a : α) → β a), x ∈ Fintype.piFinset fun x ↦ univ

Tactic:
by simp

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

Goal state before:
pp: x✝ : ℕ
⊢ x✝.multichoose 0 = (x✝ + 0 - 1).choose 0

Tactic:
by simp

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

Goal state before:
pp: k : ℕ
⊢ multichoose 0 (k + 1) = (0 + (k + 1) - 1).choose (k + 1)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ ∀ (x : α × β), x ∈ s.toFinset ×ˢ t.toFinset ↔ x ∈ s ×ˢ t

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
inst✝ : Fintype ↑s
⊢ ∀ (x : α × α), x ∈ s.toFinset.offDiag ↔ x ∈ s.offDiag

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
⊢ ∀ (a : α × β), a ∈ hs.toFinset ×ˢ ht.toFinset ↔ a ∈ ⋯.toFinset

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ ∀ (a : α × α), a ∈ ⋯.toFinset ↔ a ∈ hs.toFinset.offDiag

Tactic:
by simp

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

Goal state before:
pp: case inl
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
hG : 0 < Fintype.card G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ ∅ ^ k
k : ℕ
hk : Fintype.card G ≤ k
⊢ ↑(∅ ^ k) ≃ ↑(∅ ^ Fintype.card G)

Tactic:
rw [empty_pow (hG.trans_le hk).ne', empty_pow (ne_of_gt hG)]

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))
h₂ : S ^ n * {a} = S ^ (n + 1)
⊢ ∀ b ∈ S * S ^ n * {a}, b * a⁻¹ ∈ S ^ n * {a}

Tactic:
← pow_succ',

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 + 1) * {a}, b * a⁻¹ ∈ S ^ n * {a}
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Group α
x a b : α
⊢ (fun g ↦ x * g * x⁻¹) a = (fun g ↦ x * g * x⁻¹) b → a = b

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
x✝¹ x✝ : ↥S'
⊢ ↑(x✝¹ * x✝) = ↑x✝¹ * ↑x✝

Tactic:
by simp

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : MulOneClass M✝
inst✝¹ : SetLike A M✝
hA : SubmonoidClass A M✝
S' : A
M : Type u_4
inst✝ : MulOneClass M
S : Submonoid M
x✝¹ x✝ : ↥S
⊢ ↑(x✝¹ * x✝) = ↑x✝¹ * ↑x✝

Tactic:
by simp

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:
← (Equiv.inv _).exists_congr_right

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
p : α → Prop
⊢ (∃ a, ((Equiv.inv α) a)⁻¹ ∈ s ∧ p ((Equiv.inv α) a)) ↔ ∃ x, x ∈ s ∧ p x⁻¹
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
⊢ (s ^ 0).Nonempty

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Set α
t : Set β
⊢ s ×ˢ t ^ 0 = (s ^ 0) ×ˢ (t ^ 0)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ (fun x ↦ a⁻¹ * x) '' t = (fun x ↦ a * x) ⁻¹' t

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ (fun x ↦ x * b⁻¹) '' t = (fun x ↦ x * b) ⁻¹' t

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a : α
⊢ (fun x ↦ a⁻¹ * x) ⁻¹' 1 = {a}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
b : α
⊢ (fun x ↦ x * b⁻¹) ⁻¹' 1 = {b}

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
⊢ 1 ∈ {1}

Tactic:
by simp

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

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

pp: 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)

pp: 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)

pp: 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)

Tactic:
all_goals simp_all [mul_mem]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s * t) = s * t

Tactic:
image_preimage_eq_iff.2 (mul_subset_range m hs ht)

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ s * t = s * t
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✝ : MulHomClass F α β
x✝ : 1 ≠ 0
⊢ ∀ (f : F) (s : Set α), ⇑f '' s ^ 1 = (⇑f '' s) ^ 1

Tactic:
by simp

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

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ (x ^ (n + 1))⁻¹ ∈ K

Tactic:
exact inv_mem (pow_mem hx n.succ)

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H : Subgroup G
S : Set G
⊢ 1 ∈ {g | ∀ (n : G), n ∈ S ↔ g * n * g⁻¹ ∈ S}

Tactic:
by simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ∀ {x : G}, x ∈ ⊥.carrier → x⁻¹ ∈ ⊥.carrier

Tactic:
by simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H ≠ ⊥ ↔ ∃ a, a ≠ 1

Tactic:
rw [← nontrivial_iff_ne_bot, nontrivial_iff_exists_ne_one]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ ∃ a, a ≠ 1
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
s : Set (Subgroup G)
⊢ ⋂ S ∈ s, ↑S = ↑(⨅ S ∈ s, S.toSubmonoid)

Tactic:
by simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x✝ : Subsingleton G
x y : Subgroup G
i : G
⊢ 1 ∈ x ↔ 1 ∈ y

Tactic:
by simp

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ {x}, ∃ n, x ^ n = x_1

Tactic:
intro y hy
    rw [eq_of_mem_singleton hy]
    exact ⟨1, zpow_one x⟩

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
f : G →* N
⊢ Set.range ⇑f = ↑(map f ⊤)

Tactic:
by simp

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

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑s
⊢ y * 1 = y

Tactic:
by simp

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

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑t
⊢ 1 * y = y

Tactic:
by simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x✝ : G
hx✝ : x✝ ∈ closure (↑s ∪ ↑t)
x : G
hx : x ∈ ↑s
⊢ x * 1 = x

Tactic:
by simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x✝ : G
hx✝ : x✝ ∈ closure (↑s ∪ ↑t)
x : G
hx : x ∈ ↑t
⊢ 1 * x = x

Tactic:
by simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ 1 * 1 = 1

Tactic:
by simp

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
inst✝ : Group N
H✝ : Subgroup G
f : G →* N
H : Subgroup G
⊢ ∀ {a b : Subgroup ↥H},
    { toFun := fun H' ↦ ⟨map H.subtype H', ⋯⟩, invFun := fun sH' ↦ (↑sH').subgroupOf H, left_inv := ⋯, right_inv := ⋯ }
          a ≤
        { toFun := fun H' ↦ ⟨map H.subtype H', ⋯⟩, invFun := fun sH' ↦ (↑sH').subgroupOf H, left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by simp

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

Goal state before:
pp: P : Type u_3
inst✝ : MulOneClass P
S : Submonoid P
⊢ ∀ (x : P), x ∈ comap (MonoidHom.id P) S ↔ x ∈ S

Tactic:
by simp

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

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Set M
⊢ map (inr M N) ⊥ ≤ closure (s ×ˢ {1})

Tactic:
by simp

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

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
t : Set N
⊢ map (inl M N) ⊥ ≤ closure ({1} ×ˢ t)

Tactic:
by simp

Goal state after:
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
f : F
⊢ closure (Set.range ⇑f) = mrange f

Tactic:
← Set.image_univ,

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
f : F
⊢ closure (⇑f '' Set.univ) = mrange f
Module: Mathlib.Logic.Equiv.Nat

Goal state before:
pp: α : Type u_1
x✝ : Bool × ℕ
b : Bool
n : ℕ
⊢ (fun n ↦ (n.bodd, n.div2)) (uncurry bit (b, n)) = (b, n)

Tactic:
by simp

Goal state after:
Module: Mathlib.Logic.Equiv.Nat

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ uncurry bit ((fun n ↦ (n.bodd, n.div2)) n) = n

Tactic:
by simp

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

Goal state before:
pp: case neg
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)

Tactic:
· show unpair (a * a + a + b) = (a, b)
    have ae : sqrt (a * a + (a + b)) = a := by
      rw [sqrt_add_eq]
      exact Nat.add_le_add_left (le_of_not_gt h) _
    simp [unpair, ae, Nat.add_assoc, Nat.add_sub_cancel_left]

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

Goal state before:
pp: ⊢ (unpair 0).1 ≤ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : PUnit.{?u.4 + 1}
⊢ (Nat.casesOn 0 (some PUnit.unit) fun x ↦ none) = some x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
x✝ : (fun x ↦ x ∈ Set.range encode) x
n : α
hn : encode n = x
⊢ (decode₂ α x).isSome = true

Tactic:
rw [← hn, encodek₂]

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
x✝ : (fun x ↦ x ∈ Set.range encode) x
n : α
hn : encode n = x
⊢ (some n).isSome = true
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ decode n = (decode (unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)

Tactic:
by
  simp only [decode_ofEquiv, Equiv.symm_symm, decode_sigma_val]
  cases (decode n.unpair.1 : Option α) <;> cases (decode n.unpair.2 : Option β)
  <;> rfl

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
⊢ ∀ n ∈ ⊥, ∀ (g : G), g * n * g⁻¹ ∈ ⊥

Tactic:
by simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
⊢ H ≤ normalizer ↑(closure s) ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s

Tactic:
refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp <| mem_closure_of_mem hg, fun hH h hh ↦ ?_⟩
  rw [mem_normalizer_iff_map_conj_eq, MonoidHom.map_closure]
  apply le_antisymm <| by simpa using! hH h hh
  rw [closure_le, ← MonoidHom.map_closure]
  exact fun g hg ↦ ⟨_, hH _ (inv_mem hh) g hg, by simp [mul_assoc]⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
x b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ x • b * b⁻¹ = x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
ha : a ∈ t
hb : b ∈ s
⊢ (a * b⁻¹) • b = a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
b : α
hb : b ∈ s
h : x • b ∈ x • s
ha : x • b ∈ t
⊢ b⁻¹ * x • b = unop x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
xs : List (List α)
⊢ toList (ofList xs.flatten) = toList (List.map (⇑ofList) xs).prod

Tactic:
by simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
obtain hAB | ⟨z, hzA, hzB⟩ := (a • s ∩ b • t).eq_empty_or_nonempty
  · exact ⟨1, by simp [hAB]⟩
  refine ⟨z, ?_⟩
  calc
    a • s ∩ b • t ⊆ (z • s⁻¹) * s ∩ ((z • t⁻¹) * t) := by
      gcongr <;> apply smul_set_subset_mul <;> simpa
    _ = z • ((s⁻¹ * s) ∩ (t⁻¹ * t)) := by simp_rw [Set.smul_set_inter, smul_mul_assoc]

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 : List M
n : M
h : ∀ (x : M), x ∈ l → x ≤ n
⊢ l.prod ≤ n ^ l.length

Tactic:
simpa only [map_id', map_const', prod_replicate] using prod_le_prod' h

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
⊢ ∀ (a b : α), True → True → True

Tactic:
by simp

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
⊢ ∀ (a : α), a ∈ l → True

Tactic:
by simp

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

Goal state before:
pp: 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
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ map (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h) (normalClosure {⟨g, hg⟩}) ≤
    normalClosure {⟨c * g * c⁻¹, hg'⟩}

Tactic:
refine map_le_iff_le_comap.2 (normalClosure_le_normal ?_)

Goal state after:
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
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ {⟨g, hg⟩} ⊆
    ↑(comap (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
        (normalClosure {⟨c * g * c⁻¹, hg'⟩}))
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
⊢ ∀ x ∈ ⋃ i, ↑(S i), ∃ i, x ∈ S i

Tactic:
by simp

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

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
⊢ ∃ i, 1 ∈ S i

Tactic:
by simp

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
hs_nonempty : l ≠ ∅
⊢ ∀ (a b : α), True → True → True

Tactic:
by simp

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
l : List α
hs_nonempty : l ≠ ∅
⊢ ∀ (a : α), a ∈ l → True

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : Std.Symm r
inst✝ : ∀ (i : ι), Std.Symm (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b → Lex r s b a

Tactic:
by
    rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩)
    · exact Lex.left _ _ (symm hij)
    · exact Lex.right _ _ (symm hab)

Goal state after: