mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

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

Tactic:
by

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)
⊢ (s.pi t)⁻¹ = s.pi fun i ↦ (t i)⁻¹

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
p₁ p₂ : Submonoid M
⊢ Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
⊢ closure (s \ t) = closure s

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ {1} ⊆ ↑(closure (s \ {1}))

Tactic:
by

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
⊢ ∀ {a b : M}, a ∈ Set.ofPred IsUnit → b ∈ Set.ofPred IsUnit → a * b ∈ Set.ofPred IsUnit

Tactic:
by

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
A : Type u_3
inst✝² : Monoid M✝
inst✝¹ : Monoid N
s : Set M✝
M : Type u_4
inst✝ : Monoid M
⊢ 1 ∈ Set.ofPred IsUnit

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ submonoid M ↔ IsUnit a

Tactic:
by

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

Goal state before:
pp: S : Type u_4
M : Type u_5
inst✝² : Mul M
inst✝¹ : SetLike S M
inst✝ : MulMemClass S M
s : S
x y : ↥s
⊢ Commute ↑x ↑y ↔ Commute x y

Tactic:
by

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

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x y : M
⊢ f (1 * y) = f 1 * f y

Tactic:
by

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

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
⊢ f (a * b * y) = f (a * b) * f y

Tactic:
by

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

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x y : M
⊢ ∀ (x : M), f (x * 1) = f x * f 1

Tactic:
by

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

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x✝ y y₁ y₂ : M
h₁ : ∀ (x : M), f (x * y₁) = f x * f y₁
h₂ : ∀ (x : M), f (x * y₂) = f x * f y₂
x : M
⊢ f (x * (y₁ * y₂)) = f x * f (y₁ * y₂)

Tactic:
by

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

Goal state before:
pp: S : Type u_3
G : Type u_4
inst✝² : Inv G
inst✝¹ : SetLike S G
s : S
inst✝ : HasMemOrInvMem s
x : G
h : ¬x ∈ s
⊢ x⁻¹ ∈ s

Tactic:
by

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

Goal state before:
pp: S : Type u_3
G : Type u_4
inst✝² : Inv G
inst✝¹ : SetLike S G
s : S
inst✝ : HasMemOrInvMem s
x : G
h : ¬x⁻¹ ∈ s
⊢ x ∈ s

Tactic:
by

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
H : S
x y : M
hx : x ∈ H
hy : y ∈ H
⊢ x / y ∈ H

Tactic:
by

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

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

Goal state after:
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
P : G → Prop
x : G
x_in : x ∈ H
hx : P x⁻¹
⊢ P x⁻¹

Tactic:
by

Goal state after:
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
P : G → Prop
x : G
x_in : x ∈ H
hx : P x
⊢ P x⁻¹⁻¹

Tactic:
by

Goal state after:
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
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x⁻¹) ↔ ∃ x, x ∈ H ∧ P x

Tactic:
by

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

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

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
H K L : S
⊢ ↑H ⊆ ↑K ∪ ↑L ↔ H ≤ K ∨ H ≤ L

Tactic:
by

Goal state after:
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
⊢ ⇑↑H = Subtype.val

Tactic:
by

Goal state after:
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
inst✝¹ : Preorder S
inst✝ : IsConcreteLE S G
x : ↥H
⊢ (inclusion ⋯) x = x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H K : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
h : H ≤ K
x : ↥K
hx : ↑x ∈ H
⊢ (inclusion h) ⟨↑x, hx⟩ = x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H K : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : Preorder S
inst✝ : IsConcreteLE S G
L : S
hHK : H ≤ K
hKL : K ≤ L
x : ↥H
⊢ (inclusion hKL) ((inclusion hHK) x) = (inclusion ⋯) x

Tactic:
by

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
p q : Subgroup G
h : (fun s ↦ s.carrier) p = (fun s ↦ s.carrier) q
⊢ p = q

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
⊢ p = q

Tactic:
by

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✝ K : Subgroup G
s : Set G
hs : s = ↑K
x✝ : G
hx : x✝ ∈ s
⊢ x✝⁻¹ ∈ s

Tactic:
by

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

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
one_mem : 1 ∈ s
x : G
hx : x ∈ s
⊢ x⁻¹ ∈ s

Tactic:
by

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

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x : ↥H
n : ℤ
⊢ ↑(x ^ n) = ↑x ^ n

Tactic:
by

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
inst✝ : IsMulCommutative G
H : Subgroup G
⊢ ∀ (n : G), n ∈ H → ∀ (g : G), g * n * g⁻¹ ∈ H

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
n : G
hn : n ∈ H
g : G
⊢ g⁻¹ * n * g ∈ H

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
a b : G
h : a * b ∈ H
⊢ b * a ∈ H

Tactic:
by

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
a b : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
hb : ∀ (n : G), n ∈ S ↔ b * n * b⁻¹ ∈ S
n : G
⊢ n ∈ S ↔ a * b * n * (a * b)⁻¹ ∈ S

Tactic:
by

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

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
a : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
n : G
⊢ n ∈ S ↔ a⁻¹ * n * a⁻¹⁻¹ ∈ S

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
⊢ g ∈ normalizer S ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : g ∈ normalizer S
n : G
⊢ n * g ∈ S ↔ g * n ∈ S

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
h : ∀ (h : G), h * g ∈ S ↔ g * h ∈ S
n : G
⊢ n ∈ S ↔ g * n * g⁻¹ ∈ S

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
⊢ n ∈ ↑H ↔ x * n * x⁻¹ ∈ ↑H

Tactic:
by

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

Goal state before:
pp: F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : InjOn ⇑f ↑s
a : G
ha : a ∈ s
ha' : f a = 1
⊢ a = 1

Tactic:
by

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

Goal state before:
pp: F : Type u_3
G : Type u_4
H : Type u_5
S : Type u_6
inst✝⁷ : Group G
inst✝⁶ : Group H
inst✝⁵ : FunLike F G H
inst✝⁴ : MonoidHomClass F G H
f : F
inst✝³ : SetLike S G
inst✝² : OneMemClass S G
inst✝¹ : MulMemClass S G
inst✝ : InvMemClass S G
s : S
h : ∀ (a : G), a ∈ s → f a = 1 → a = 1
x : G
hx : x ∈ ↑s
y : G
hy : y ∈ ↑s
hxy : f x = f y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : Subgroup G
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        x) =
    x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : AddSubgroup (Additive G)
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        x) =
    x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : AddSubgroup A
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        x) =
    x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : Subgroup (Multiplicative A)
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        x) =
    x

Tactic:
by

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

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
⊢ H = ⊥

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ↑H = ↑⊤ ↔ ↑H = Set.univ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : ∃ g, ↑H = {g}
g : G
hg : ↑H = {g}
⊢ Subsingleton ↑↑H

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ ∃ x ∈ H, x ≠ 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Nontrivial ↥H
⊢ ∃ x ∈ H, x ≠ 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ H ≠ ⊥

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H = ⊥ ∨ Nontrivial ↥H

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H = ⊥ ∨ ∃ x ∈ H, x ≠ 1

Tactic:
by

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

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

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)
x : G
hx : x ∈ ((⨅ S ∈ s, S.toSubmonoid).copy (⋂ S ∈ s, ↑S) ⋯).carrier
i : Subgroup G
h : i ∈ s
⊢ x ∈ i

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
S : ι → Subgroup G
x : G
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
S : ι → Subgroup G
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
by

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

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Nontrivial G
⊢ Nontrivial ↥⊤

Tactic:
by

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

Goal state before:
pp: 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
hy : y ∈ closure k
⊢ p x y hx hy

Tactic:
by

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 ⊔ H' = closure (↑H ∪ ↑H')

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
p : ι → Subgroup G
⊢ ⨆ i, p i = closure (⋃ i, ↑(p i))

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
⊢ y ∈ closure {x} ↔ ∃ n, x ^ n = y

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ closure {1} = ⊥

Tactic:
by

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

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (insert 1 s) = closure s

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (s ∪ {1}) = closure s

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (s \ {1}) = closure s

Tactic:
by

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

Goal state before:
pp: N : Type u_5
inst✝ : Group N
K : Subgroup N
⊢ comap (MonoidHom.id N) K = K

Tactic:
by

Goal state after:
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
f : G →* N
H : Subgroup G
⊢ ∀ {x : N}, x ∈ ⇑f '' ↑H → x⁻¹ ∈ ⇑f '' ↑H

Tactic:
by

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
⊢ map 1 K ≤ ⊥

Tactic:
by

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

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
H : Subgroup N
e : G ≃* N
⊢ map (↑e.symm) H = K ↔ map (↑e) K = H

Tactic:
by

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

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
H K : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ map f (H ⊓ K) = map f H ⊓ map f K

Tactic:
by

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
f : G →* N
hf : Injective ⇑f
H K : Subgroup G
h : Disjoint H K
⊢ Disjoint (map f H) (map f K)

Tactic:
by

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
f : G →* N
h : Surjective ⇑f
⊢ map f ⊤ = ⊤

Tactic:
by

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
f : G →* N
hf : Surjective ⇑f
H K : Subgroup G
h : Codisjoint H K
⊢ Codisjoint (map f H) (map f K)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ↑(map K.subtype (H.subgroupOf K)) = ↑(H ⊓ K)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ map K.subtype (H.subgroupOf K) = H

Tactic:
by

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

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

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (K ⊓ H).subgroupOf K = H.subgroupOf K

Tactic:
by

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
⊢ f.range = map f ⊤

Tactic:
by

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
⊢ comap f f.range = ⊤

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊥ ↔ Disjoint H K

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊤ ↔ K ≤ H

Tactic:
by

Goal state after:
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
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i ↔ ∃ i, p i ∧ x ∈ K i

Tactic:
by

Goal state after: