mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case nil
α : Type u
k : ℕ
⊢ ([].rotate k).cyclicPermutations.length = ([].cyclicPermutations.rotate k).length

Tactic:
simp

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

Goal state before:
pp: case cons
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ ((head✝ :: tail✝).rotate k).length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length

Tactic:
simp

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

Goal state before:
pp: case cons.h
α : Type u
k : ℕ
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).rotate k ≠ []

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).bind fun a ↦ map (Sigma.mk a) ↑(l₂ a)) = (↑l₁).bind fun a ↦ ↑(List.map (Sigma.mk a) (l₂ a))

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u
k n : ℕ
this : ([].rotate k).cyclicPermutations.length = ([].cyclicPermutations.rotate k).length
hn : n < ([].rotate k).cyclicPermutations.length
hn' : n < ([].cyclicPermutations.rotate k).length
⊢ [].rotate ((↑⟨n, hn⟩ + k) % [].length) = [].cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % [].cyclicPermutations.length, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: case cons
α : Type u
k n : ℕ
head✝ : α
tail✝ : List α
this : ((head✝ :: tail✝).rotate k).cyclicPermutations.length = ((head✝ :: tail✝).cyclicPermutations.rotate k).length
hn : n < ((head✝ :: tail✝).rotate k).cyclicPermutations.length
hn' : n < ((head✝ :: tail✝).cyclicPermutations.rotate k).length
⊢ (head✝ :: tail✝).rotate ((↑⟨n, hn⟩ + k) % (head✝ :: tail✝).length) =
    (head✝ :: tail✝).cyclicPermutations.get ⟨(↑⟨n, hn'⟩ + k) % (head✝ :: tail✝).cyclicPermutations.length, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u
hn : [].Nodup
⊢ [].cyclicPermutations.Nodup

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
a b : α
⊢ count (a, b) [].offDiag = count a [] * count b [] - if a = b then count a [] else 0

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = count x l

Tactic:
rw [h, count_map_of_injective l (·, y) (by simp [Function.Injective])]

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

Goal state before:
pp: case zero
⊢ choose 0 2 = 0 * (0 - 1) / 2

Tactic:
simp

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

Goal state before:
pp: n : ℕ
x✝ : 0 ≤ n + 1
⊢ 0 < (n + 1).choose 0

Tactic:
simp

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

Goal state before:
pp: n : ℕ
x✝ : 0 ≤ n + 1
⊢ (n + 1).choose 0 * 0! * (n + 1 - 0)! = (n + 1)!

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
a✝ : α × β
⊢ a✝ ∈ (s ×ˢ t).toFinset ↔ a✝ ∈ s.toFinset ×ˢ t.toFinset

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑s.offDiag
⊢ ∀ (a : α × α), a ∈ s.offDiag.toFinset ↔ a ∈ s.toFinset.offDiag

Tactic:
simp

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝ : α × β
a : α
b : β
⊢ (a, b) ∈ univ ×ˢ univ

Tactic:
simp

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:
simp

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

Goal state before:
pp: case zero
n : ℕ
⊢ n.choose 0 * (n + 1) = (n + 1).choose 0 * (n + 1 - 0)

Tactic:
simp

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:
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:
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:
simp

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
a : α
this : Nonempty α
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ ∅) = ∅

Tactic:
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:
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:
simp

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

Goal state before:
pp: α : Type u_3
β : α → Type u_4
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
a✝ : (a : α) → a ∈ univ → β a
⊢ (a✝ ∈ univ.pi fun a ↦ univ) ↔ a✝ ∈ univ

Tactic:
simp

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

Goal state before:
pp: case zero
a c : ℕ
⊢ a.choose c ≤ (a + 0).choose c

Tactic:
simp

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

Goal state before:
pp: a b c : ℕ
⊢ a.choose c ≤ (a + b).choose c

Tactic:
induction b with
  | zero => simp
  | succ b_n b_ih => exact b_ih.trans (choose_le_succ (a + b_n) c)

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

Goal state before:
pp: case inr.inl
k : ℕ
⊢ k.choose k = 1 ↔ k = 0 ∨ k = k

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ multichoose 1 0 = 1

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ multichoose 2 0 = 0 + 1

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ multichoose 0 1 = 0

Tactic:
simp

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

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

Tactic:
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:
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:
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:
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:
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:
simp

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

Goal state before:
pp: case h
G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
x y : α
⊢ swap x y • x = y

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u
inst✝ : Group α
a b : α
⊢ (a * b * a⁻¹) ^ 0 = a * b ^ 0 * a⁻¹

Tactic:
simp

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

Goal state before:
pp: case ofNat
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.ofNat a✝ = a * b ^ Int.ofNat a✝ * a⁻¹

Tactic:
simp

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
x✝ : α
⊢ x✝ ∈ f ⁻¹' ⋂ i, s i ↔ x✝ ∈ ⋂ i, f ⁻¹' s i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
x✝ : α × β
⊢ x✝ ∈ s ×ˢ ⋃ i, t i ↔ x✝ ∈ ⋃ i, s ×ˢ t i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ (⋃ i, s i) ×ˢ t ↔ x✝ ∈ ⋃ i, s i ×ˢ t

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → Mul (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
I : Type u_7
x✝² x✝¹ : I → α
x✝ : I
⊢ (⇑f ∘ (x✝² * x✝¹)) x✝ = (⇑f ∘ x✝² * ⇑f ∘ x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_9
ι' : Type u_10
α : Type u_11
β : Type u_12
s : ι → Set α
t : ι' → Set β
x✝ : α × β
⊢ x✝ ∈ ⋃ x, s x.1 ×ˢ t x.2 ↔ x✝ ∈ (⋃ i, s i) ×ˢ ⋃ i, t i

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_7
x✝ : I
⊢ (⇑f ∘ 1) x✝ = 1 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_7
x✝² x✝¹ : I → α
x✝ : I
⊢ (⇑f ∘ (x✝² * x✝¹)) x✝ = (⇑f ∘ x✝² * ⇑f ∘ x✝¹) x✝

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
⊢ w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i

Tactic:
hw

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
hw : w ∈ t x
⊢ (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
p : α → Prop
⊢ (∃ a, ((Equiv.inv α) a)⁻¹ ∈ s ∧ p ((Equiv.inv α) a)) ↔ ∃ x, x ∈ s ∧ p x⁻¹

Tactic:
simp

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

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
x' : α
⊢ w ∈ t x' → ∃ i, z ∈ s i ∧ w ∈ t i

Tactic:
hw

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
x' : α
hw : w ∈ t x'
⊢ ∃ i, z ∈ s i ∧ w ∈ t i
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case inl
I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
⊢ Function.update g i x i = (g / mulSingle i (g i) * mulSingle i x) i

Tactic:
simp

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

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

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

Tactic:
simp

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

Goal state before:
pp: case hab
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ s ∩ t ⊆ s

Tactic:
simp

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

Goal state before:
pp: case hab
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ s ∩ t ⊆ t

Tactic:
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:
simp

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

Goal state before:
pp: case 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
⊢ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1

Tactic:
refine ⟨a, b, ?_, ?_, H ha hb⟩

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
⊢ s = {a}

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}
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ ⋃ b ∈ t, (fun x ↦ f x b) '' s = image2 f s t

Tactic:
rw [image2_swap, iUnion_image_left]

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

Goal state before:
pp: case mp.inr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (s ^ 0).Nonempty

Tactic:
simp

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

Goal state before:
pp: case ofNat
α : Type u_2
inst✝ : DivisionMonoid α
a : α
a✝ : ℕ
⊢ {a} ^ Int.ofNat a✝ = {a ^ Int.ofNat a✝}

Tactic:
simp

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

Goal state before:
pp: case negSucc
α : Type u_2
inst✝ : DivisionMonoid α
a : α
a✝ : ℕ
⊢ {a} ^ Int.negSucc a✝ = {a ^ Int.negSucc a✝}

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
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:
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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x * b) ((fun x ↦ x / b) c) = c

Tactic:
simp

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

Goal state before:
pp: case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b c : α
⊢ (fun x ↦ x / b) ((fun x ↦ x * b) c) = c

Tactic:
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:
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:
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:
simp

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✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
x✝ : 1 ≠ 0
⊢ ∀ (f : F) (s : Set α), ⇑f '' s ^ 1 = (⇑f '' s) ^ 1

Tactic:
simp

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

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → Inv (α i)
s : Set ι
t : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ x ∈ (s.pi t)⁻¹ ↔ x ∈ s.pi fun i ↦ (t i)⁻¹

Tactic:
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 ∈ K

Tactic:
by
    rw [zpow_natCast]
    exact pow_mem hx n

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 K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
⊢ 1 ∈ s

Tactic:
let ⟨x, hx⟩ := hsn
    simpa using hs x hx x hx

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:
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:
simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ y, ∃ (_ : y ∈ H), y ≠ ↑1) ↔ ∃ x ∈ H, x ≠ 1

Tactic:
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
s : Set (Subgroup G)
⊢ ⋂ S ∈ s, ↑S = ↑(⨅ S ∈ s, S.toSubmonoid)

Tactic:
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:
simp

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

Goal state before:
pp: case inv
G : Type u_1
inst✝ : Group G
k : Set G
p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : x ∈ closure k), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : x ∈ closure k), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : x ∈ closure k
x✝ : G
hx✝ : x✝ ∈ closure k
h : p x x✝ hx hx✝
⊢ p x x✝⁻¹ hx ⋯

Tactic:
exact inv_right _ _ _ _ h

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
y : G
left✝ : y ∈ ↑K
⊢ 1 y ∈ ⊥

Tactic:
simp

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

Goal state before:
pp: case refine_1.refine_1
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
x✝ : G
⊢ x✝ ∈ ⋃ i, ⋃ (_ : p i), ↑(K i) → ∃ i, p i ∧ x✝ ∈ K i

Tactic:
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
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
K : Subgroup G
f : G →* N
⊢ Set.range ⇑f = ↑(map f ⊤)

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
x✝ : N
⊢ x✝ ∈ f.range ↔ x✝ ∈ map f ⊤

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
x✝ : G
⊢ x✝ ∈ comap f f.range ↔ x✝ ∈ ⊤

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
⊢ (∃ i, True ∧ x ∈ K i.down) ↔ ∃ i, x ∈ K i

Tactic:
simp

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

Goal state before:
pp: case hK
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
i : PLift ι
⊢ ∀ (y : PLift ι), ∃ x, K i.down ≤ K x ∧ K y.down ≤ K x

Tactic:
intro j

Goal state after:
case hK
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
i j : PLift ι
⊢ ∃ x, K i.down ≤ K x ∧ K j.down ≤ K x
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case hK
G : Type u_1
inst✝ : Group G
ι : Sort u_2
hι : Nonempty ι
K : ι → Subgroup G
hK : Directed (fun x1 x2 ↦ x1 ≤ x2) K
x : G
this : iSup K = ⨆ i, ⨆ (_ : True), K i.down
i j : PLift ι
⊢ ∀ (a : ι),
    (fun x1 x2 ↦ x1 ≤ x2) (K i.down) (K a) ∧ (fun x1 x2 ↦ x1 ≤ x2) (K j.down) (K a) → K i.down ≤ K a ∧ K j.down ≤ K a

Tactic:
simp

Goal state after: