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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ n ≤ (a :: l).length

Tactic:
simpa using

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ n ≤ l.length + 1
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
h : l.cyclicPermutations = l'.cyclicPermutations
⊢ l = l'

Tactic:
simpa using

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

Goal state before:
pp: α : Type u
l : List α
⊢ l ∈ l.cyclicPermutations

Tactic:
simpa using

Goal state after:
α : Type u
l : List α
⊢ l ∈ l.cyclicPermutations
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
t : Finset α
f : α → Finset β
⊢ Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
t : Finset α
f : α → Finset β
⊢ Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i)
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
s : Multiset α
σ : α → Type u_5
t : (a : α) → Multiset (σ a)
l₁ : List α
f : (a : α) → List (σ a)
hf : ∀ (a : α), ⟦f a⟧ = t a
⊢ Nodup (Quot.mk (⇑(List.isSetoid α)) l₁) →
    (∀ (a : α), (t a).Nodup) → (Multiset.sigma (Quot.mk (⇑(List.isSetoid α)) l₁) t).Nodup

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Multiset α
σ : α → Type u_5
t : (a : α) → Multiset (σ a)
l₁ : List α
f : (a : α) → List (σ a)
hf : ∀ (a : α), ⟦f a⟧ = t a
⊢ l₁.Nodup → (∀ (a : α), (f a).Nodup) → (l₁.sigma f).Nodup
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi✝ : i < l.cyclicPermutations.length
j : ℕ
hj✝ : j < l.cyclicPermutations.length
h : l.cyclicPermutations.get ⟨i, hi✝⟩ = l.cyclicPermutations.get ⟨j, hj✝⟩
hi : i < l.length
hj : j < l.length
⊢ ⟨i, hi✝⟩ = ⟨j, hj✝⟩

Tactic:
simpa using

Goal state after:
case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi✝ : i < l.cyclicPermutations.length
j : ℕ
hj✝ : j < l.cyclicPermutations.length
h : l.cyclicPermutations.get ⟨i, hi✝⟩ = l.cyclicPermutations.get ⟨j, hj✝⟩
hi : i < l.length
hj : j < l.length
⊢ i = j
Module: Mathlib.Data.List.Rotate

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

Tactic:
exact ⟨k, by simp⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : LinearOrder α
⊢ #{x | x.1 < x.2} = (card α).choose 2

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : LinearOrder α
⊢ #{x | x.1 < x.2} = (card α).choose 2
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α ↪ β
g : γ ↪ δ
s : Finset α
t : Finset γ
⊢ map (f.prodMap g) (s ×ˢ t) = map f s ×ˢ map g t

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α ↪ β
g : γ ↪ δ
s : Finset α
t : Finset γ
⊢ Prod.map ⇑f ⇑g '' ↑s ×ˢ ↑t = (⇑f '' ↑s) ×ˢ (⇑g '' ↑t)
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
inst✝ : DecidablePred p
⊢ {x ∈ s ×ˢ t | p x.1} = filter p s ×ˢ t

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
inst✝ : DecidablePred p
⊢ {x ∈ s ×ˢ t | p x.1} = filter p s ×ˢ t
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
q : β → Prop
inst✝ : DecidablePred q
⊢ {x ∈ s ×ˢ t | q x.2} = s ×ˢ filter q t

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
q : β → Prop
inst✝ : DecidablePred q
⊢ {x ∈ s ×ˢ t | q x.2} = s ×ˢ filter q t
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: ι : Type u_4
inst✝² : PartialOrder ι
inst✝¹ : DecidableLE ι
inst✝ : DecidableLT ι
s : Finset ι
a✝ : ι × ι
⊢ a✝ ∈ {i ∈ s.offDiag | i.1 < i.2} ↔ a✝ ∈ {i ∈ s.offDiag | i.1 ≤ i.2}

Tactic:
simpa using

Goal state after:
ι : Type u_4
inst✝² : PartialOrder ι
inst✝¹ : DecidableLE ι
inst✝ : DecidableLT ι
s : Finset ι
a✝ : ι × ι
⊢ a✝.1 ∈ s → a✝.2 ∈ s → ¬a✝.1 = a✝.2 → (a✝.1 < a✝.2 ↔ a✝.1 ≤ a✝.2)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case self
n r : ℕ
⊢ n.choose (n / 2) ≤ n.choose (n / 2)

Tactic:
| self =>

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

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
⊢ {f | ∀ (i : ι), f i ∈ t i}.Finite

Tactic:
simpa using

Goal state after:
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
⊢ {f | ∀ (i : ι), f i ∈ t i}.Finite
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝² x✝¹ : N
x✝ : α
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
simpa using

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝² x✝¹ : N
x✝ : α
⊢ SMul.smul (g x✝² * g x✝¹) x✝ = SMul.smul (g x✝²) (SMul.smul (g x✝¹) x✝)
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝ : α
⊢ 1 • x✝ = x✝

Tactic:
simpa using

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝ : α
⊢ SMul.smul 1 x✝ = x✝
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k = v i

Tactic:
apply Subset.antisymm

Goal state after:
case h₁
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k ⊆ v i

case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ v i ⊆ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
j : ι
x✝ : j ≠ i
⊢ z j ∈ v j

Tactic:
simpa using

Goal state after:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
j : ι
x✝ : j ≠ i
⊢ z j ∈ v j
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Surjective f ↔ ∀ (i : ι), Surjective ((U i).restrictPreimage f)

Tactic:
refine ⟨fun H i => (U i).restrictPreimage_surjective H, fun H x => ?_⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ InjOn f (⋃ i, s ↑i ⋯)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ InjOn f (⨆ i, s ↑i ⋯)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ i, s i
y : α
hy : y ∈ ⋃ i, s i
hxy : f x = f y
i : ι
hx : x ∈ s i
⊢ x = y

Tactic:
rcases mem_iUnion.1 hy with ⟨j, hy⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ i, s i
y : α
hy✝ : y ∈ ⋃ i, s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ x = y
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set α
⊢ f '' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f '' s i j

Tactic:
by simp_rw [image_iUnion]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ ⋃ x, ⋃ y, ⋃ (_ : f y = x), g x = ⋃ y, g (f y)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ ⋃ x, ⋃ y, ⋃ (_ : f y = x), g x = ⋃ y, g (f y)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ ⋂ x, ⋂ y, ⋂ (_ : f y = x), g x = ⋂ y, g (f y)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ ⋂ x, ⋂ y, ⋂ (_ : f y = x), g x = ⋂ y, g (f y)
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 _).forall_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 α
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
a : α
n : ℕ
ha : a ∈ s
⊢ a ^ n ∈ s ^ n

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Monoid α
s : Set α
a : α
n : ℕ
ha : a ∈ s
⊢ a ^ n ∈ s ^ n
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
η : Type v
R : Type w
s : ι → η
inst✝ : MulOneClass R
f g : ι → R
⊢ extend s (f * g) 1 = extend s f 1 * extend s g 1

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
I : Type u
f✝ : I → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I
η : Type v
R : Type w
s : ι → η
inst✝ : MulOneClass R
f g : ι → R
⊢ extend s (f * g) 1 = extend s f 1 * extend s g 1
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
hs : 1 ∈ s
⊢ 1 ∈ s ^ n

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
hs : 1 ∈ s
⊢ 1 ∈ s ^ n
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CancelMonoid α
s : Set α
hs : s.Nontrivial
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (s ^ (n + 2)).Nontrivial

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : CancelMonoid α
s : Set α
hs : s.Nontrivial
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (s ^ n * s * s).Nontrivial
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ Int.negSucc n).Nonempty

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ (n + 1)).Nonempty
Module: Mathlib.Algebra.Group.Submonoid.Basic

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

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ {1}
⊢ x = 1
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 β
n : ℕ
⊢ (⇑f ⁻¹' s) ^ (n + 1) ⊆ ⇑f ⁻¹' s ^ (n + 1)

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set β
n : ℕ
⊢ (⇑f ⁻¹' s) ^ n * ⇑f ⁻¹' s ⊆ ⇑f ⁻¹' (s ^ n * s)
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
x y : G
h : x ∈ H
hba : y * x ∈ H
⊢ y ∈ H

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
x y : G
h : x ∈ H
hba : y * x ∈ H
⊢ y ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
x y : G
h : x ∈ H
hab : x * y ∈ H
⊢ y ∈ H

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
x y : G
h : x ∈ H
hab : x * y ∈ H
⊢ y ∈ H
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✝ K : Subgroup G
s : Set G
hs : s = ↑K
x✝ : G
hx : x✝ ∈ s
⊢ x✝⁻¹ ∈ s

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K✝ K : Subgroup G
s : Set G
hs : s = ↑K
x✝ : G
hx : x✝ ∈ s
⊢ x✝ ∈ K
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
x : G
hx : x ∈ s
⊢ 1 ∈ s

Tactic:
simpa using

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

Tactic:
simpa using

Goal state after:
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
one_mem : 1 ∈ s
x : G
hx : x ∈ s
⊢ x⁻¹ ∈ 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
H K : Subgroup G
s : Set G
hsn : s.Nonempty
hs : ∀ (x : G), x ∈ s → ∀ (y : G), y ∈ s → x * y⁻¹ ∈ s
one_mem : 1 ∈ s
inv_mem : ∀ (x : G), x ∈ s → x⁻¹ ∈ s
a✝ b✝ : G
hx : a✝ ∈ s
hy : b✝ ∈ s
⊢ a✝ * b✝ ∈ s

Tactic:
simpa using

Goal state after:
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
one_mem : 1 ∈ s
inv_mem : ∀ (x : G), x ∈ s → x⁻¹ ∈ s
a✝ b✝ : G
hx : a✝ ∈ s
hy : b✝ ∈ s
⊢ a✝ * b✝ ∈ s
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:
by
  rw [← nontrivial_iff_ne_bot, nontrivial_iff_exists_ne_one]
  simp only [ne_eq, Subtype.exists, mk_eq_one, exists_prop]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
⊢ x ∈ closure {x}

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
⊢ x ∈ closure {x}
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: 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
this : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) → ∃ i, p i ∧ x ∈ K i
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i → ∃ i, p i ∧ x ∈ K i

Tactic:
simpa using

Goal state after:
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
this : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) → ∃ i, p i ∧ x ∈ K i
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i → ∃ i, p i ∧ x ∈ K i
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:
simpa using

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
⊢ ⇑f '' ⋂ i, ↑(s i) = ⋂ i, ⇑f '' ↑(s i)
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ K : Subgroup G
⊢ H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ K : Subgroup G
⊢ (∀ (x : ↥K), ↑x ∈ H₁ ↔ ↑x ∈ H₂) ↔ ∀ x ∈ K, x ∈ H₁ ↔ x ∈ H₂
Module: Mathlib.Algebra.Group.Subgroup.Map

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
k : Set G
N : Type u_5
inst✝² : Group N
P : Type u_6
inst✝¹ : Group P
H : Subgroup G
f : G →* G'
inst✝ : IsMulCommutative ↥H
a : G
ha : a ∈ ↑H
b : G
hb : b ∈ ↑H
⊢ f a * f b = f b * f a

Tactic:
simpa using

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
k : Set G
N : Type u_5
inst✝² : Group N
P : Type u_6
inst✝¹ : Group P
H : Subgroup G
f : G →* G'
inst✝ : IsMulCommutative ↥H
a : G
ha : a ∈ ↑H
b : G
hb : b ∈ ↑H
⊢ f a * f b = f b * f a
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H : Subgroup G
f : G' →* G
hf : Injective ⇑f
inst✝ : IsMulCommutative ↥H
a : G'
ha : f a ∈ H
b : G'
hb : f b ∈ H
⊢ f (a * b) = f (b * a)

Tactic:
simpa using

Goal state after:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H : Subgroup G
f : G' →* G
hf : Injective ⇑f
inst✝ : IsMulCommutative ↥H
a : G'
ha : f a ∈ H
b : G'
hb : f b ∈ H
⊢ f a * f b = f b * f a
Module: Mathlib.Algebra.Group.Subgroup.Map

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 : Type u_5
inst✝ : Group H
f : G ≃* H
sg1 sg2 : Subgroup H
h :
  { toFun := Subgroup.comap ↑f, invFun := Subgroup.comap ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg1 ≤
    { toFun := Subgroup.comap ↑f, invFun := Subgroup.comap ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg2
⊢ sg1 ≤ sg2

Tactic:
simpa using

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 : Type u_5
inst✝ : Group H
f : G ≃* H
sg1 sg2 : Subgroup H
h :
  { toFun := Subgroup.comap ↑f, invFun := Subgroup.comap ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg1 ≤
    { toFun := Subgroup.comap ↑f, invFun := Subgroup.comap ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg2
⊢ sg1 ≤ sg2
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
x : N
⊢ x ∈ range 1 ↔ x ∈ ⊥

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
x : N
⊢ 1 = x ↔ x = 1
Module: Mathlib.Algebra.Group.Subgroup.Map

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✝ : Type u_5
inst✝¹ : Group H✝
H : Type u_6
inst✝ : Group H
f : G ≃* H
sg1 sg2 : Subgroup G
h :
  { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg1 ≤
    { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg2
⊢ sg1 ≤ sg2

Tactic:
simpa using

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✝ : Type u_5
inst✝¹ : Group H✝
H : Type u_6
inst✝ : Group H
f : G ≃* H
sg1 sg2 : Subgroup G
h :
  { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg1 ≤
    { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯ } sg2
⊢ sg1 ≤ sg2
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 ∈ s ⊔ t
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
by
    rw [sup_eq_closure] at h
    refine Subgroup.closure_induction ?_ ?_ ?_ ?_ h
    · rintro y (h | h)
      · exact ⟨y, h, 1, t.one_mem, by simp⟩
      · exact ⟨1, s.one_mem, y, h, by simp⟩
    · exact ⟨1, s.one_mem, 1, ⟨t.one_mem, mul_one 1⟩⟩
    · rintro _ _ _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
      exact ⟨_, mul_mem hy₁ hy₂, _, mul_mem hz₁ hz₂, by simp [mul_assoc, mul_left_comm]⟩
    · rintro _ _ ⟨y, hy, z, hz, rfl⟩
      exact ⟨_, inv_mem hy, _, inv_mem hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
hxy : x * y = 1
hx1 : x = 1 := h hx (Subgroup.inv_mem H₂ hy) (eq_inv_iff_mul_eq_one.mpr hxy)
⊢ y = 1

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
hxy : x * y = 1
hx1 : x = 1 := h hx (Subgroup.inv_mem H₂ hy) (eq_inv_iff_mul_eq_one.mpr hxy)
⊢ y = 1
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:
simpa using

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
⊢ ⇑f '' ⋂ i, ↑(s i) = ⋂ i, ⇑f '' ↑(s i)
Module: Mathlib.Data.Countable.Defs

Goal state before:
pp: α : Sort u
⊢ ¬Uncountable α ↔ Countable α

Tactic:
uncountable_iff_not_countable,

Goal state after:
α : Sort u
⊢ ¬¬Countable α ↔ Countable α
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 : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
⊢ (inl M N) x1 ∈ map (inl M N) s

Tactic:
simpa using

Goal state after:
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
⊢ x1 ∈ s
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 : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
h1' : (inl M N) x1 ∈ u
⊢ (inr M N) x2 ∈ map (inr M N) t

Tactic:
simpa using

Goal state after:
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
h1' : (inl M N) x1 ∈ u
⊢ x2 ∈ t
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 : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
hH : map (inl M N) s ≤ u
hK : map (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ ↑s
h2 : (x1, x2).2 ∈ ↑t
h1' : (inl M N) x1 ∈ u
⊢ (inr M N) x2 ∈ map (inr M N) t

Tactic:
simpa using h2

Goal state after: