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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ a⁻¹ * x) '' s ∩ t).Nonempty ↔ ((fun x ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
rw [← nonempty_inv, inter_inv]

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun x ↦ a⁻¹ * x) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun x ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun x ↦ x * a⁻¹) '' s ∩ t).Nonempty ↔ ((fun x ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
rw [← nonempty_inv, inter_inv]

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun x ↦ x * a⁻¹) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun x ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ image2 f (⋂ i, s i) t ⊆ ⋂ i, image2 f (s i) t

Tactic:
simp_rw [image2_subset_iff, mem_iInter]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι), x ∈ s i) → ∀ y ∈ t, ∀ (i : ι), f x y ∈ image2 f (s i) t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ image2 f s (⋂ i, t i) ⊆ ⋂ i, image2 f s (t i)

Tactic:
simp_rw [image2_subset_iff, mem_iInter]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι), y ∈ t i) → ∀ (i : ι), f x y ∈ image2 f s (t i)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ image2 f (⋂ i, ⋂ j, s i j) t ⊆ ⋂ i, ⋂ j, image2 f (s i j) t

Tactic:
simp_rw [image2_subset_iff, mem_iInter]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι) (i_1 : κ i), x ∈ s i i_1) → ∀ y ∈ t, ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f (s i i_1) t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ image2 f s (⋂ i, ⋂ j, t i j) ⊆ ⋂ i, ⋂ j, image2 f s (t i j)

Tactic:
simp_rw [image2_subset_iff, mem_iInter]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : Set α
t : (i : ι) → κ i → Set β
⊢ ∀ x ∈ s, ∀ (y : β), (∀ (i : ι) (i_1 : κ i), y ∈ t i i_1) → ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f s (t i i_1)
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

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

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

Tactic:
·

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

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

Tactic:
·

Goal state after:
case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
·

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp.inl
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

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

Tactic:
·

Goal state after:
case mp.inl
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
hs : s.Nonempty
⊢ (s ^ n).Nonempty
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:
·

Goal state after:
case mp.inr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (s ^ 0).Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
·

Goal state after:
case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ ↑(closure s) ⊆ {1} ∪ ↑(Subsemigroup.closure s)

pp: case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ {1} ∪ ↑(Subsemigroup.closure s) ⊆ ↑(closure s)

Tactic:
·

Goal state after:
case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ ↑(closure s) ⊆ {1} ∪ ↑(Subsemigroup.closure s)
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ ↑(closure s)
⊢ x ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
induction hx using closure_induction with
    | mem x hx => exact Or.inr <| Subsemigroup.subset_closure hx
    | one => exact Or.inl <| by simp
    | mul x hx y hy hx hy =>
      push _ ∈ _ at hx hy
      obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
      all_goals simp_all [mul_mem]

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

Goal state before:
pp: case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ {1} ∪ ↑(Subsemigroup.closure s) ⊆ ↑(closure s)

Tactic:
·

Goal state after:
case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ {1} ∪ ↑(Subsemigroup.closure s) ⊆ ↑(closure s)
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case a.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ {1}
⊢ x ∈ ↑(closure s)

pp: case a.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ ↑(Subsemigroup.closure s)
⊢ x ∈ ↑(closure s)

Tactic:
·

Goal state after:
case a.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ {1}
⊢ x ∈ ↑(closure s)
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case a.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ ↑(Subsemigroup.closure s)
⊢ x ∈ ↑(closure s)

Tactic:
·

Goal state after:
case a.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ ↑(Subsemigroup.closure s)
⊢ x ∈ ↑(closure s)
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case pos
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
hxt : x ∈ t
⊢ x ∈ ↑(closure (s \ t))

pp: case neg
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
hxt : x ∉ t
⊢ x ∈ ↑(closure (s \ t))

Tactic:
·

Goal state after:
case pos
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
hxt : x ∈ t
⊢ x ∈ ↑(closure (s \ t))
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case neg
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
hxt : x ∉ t
⊢ x ∈ ↑(closure (s \ t))

Tactic:
·

Goal state after:
case neg
M : Type u_1
inst✝ : MulOneClass M
s t : Set M
hts : t ⊆ ↑(closure (s \ t))
x : M
hxs : x ∈ s
hxt : x ∉ t
⊢ x ∈ ↑(closure (s \ t))
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
  refine (closure_mono Set.sdiff_subset).antisymm <| closure_le.mpr <| fun x hxs ↦ ?_
  by_cases hxt : x ∈ t
  · exact hts hxt
  · rw [SetLike.mem_coe, Submonoid.mem_closure]
    exact fun N hN ↦ hN <| Set.mem_sdiff_of_mem hxs hxt

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

Goal state before:
pp: case mp
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:
·

Goal state after:
case mp
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
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: case mpr
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:
·

Goal state after:
case mpr
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⁻¹
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
  convert! H.bot_or_nontrivial
  rw [nontrivial_iff_exists_ne_one]

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

pp: case refine_2
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∃ n, x ^ n = 1

pp: case refine_3
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), x_1 ∈ closure {x} → y ∈ closure {x} → (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y

pp: case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ closure {x}, (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹

Tactic:
·

Goal state after:
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
Module: Mathlib.Algebra.Group.Subgroup.Lattice

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

pp: case refine_3
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), x_1 ∈ closure {x} → y ∈ closure {x} → (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y

pp: case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ closure {x}, (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∃ n, x ^ n = 1
Module: Mathlib.Algebra.Group.Subgroup.Lattice

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

pp: case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ closure {x}, (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹

Tactic:
·

Goal state after:
case refine_3
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), x_1 ∈ closure {x} → y ∈ closure {x} → (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y
Module: Mathlib.Algebra.Group.Subgroup.Lattice

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

pp: case refine_2
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 ∧ x ∈ K i
i : ι
hi' : p i
hi : x ∈ K i
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i

Tactic:
·

Goal state after:
case 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
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i → ∃ i, p i ∧ x ∈ K i
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e) (map (↑e.symm) H) = H

pp: case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (↑e.symm) (map (↑e) K) = K

Tactic:
·

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e) (map (↑e.symm) H) = H
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (↑e.symm) (map (↑e) K) = K

Tactic:
·

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (↑e.symm) (map (↑e) K) = K
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

pp: case refine_1.refine_2
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))
⊢ ∃ i, p i ∧ 1 ∈ K i

pp: case refine_1.refine_3
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 y : G),
    x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) →
      y ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) → (∃ i, p i ∧ x ∈ K i) → (∃ i, p i ∧ y ∈ K i) → ∃ i, p i ∧ x * y ∈ K i

pp: case refine_1.refine_4
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 ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)), (∃ i, p i ∧ x ∈ K i) → ∃ i, p i ∧ x⁻¹ ∈ K i

Tactic:
·

Goal state after:
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
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_1.refine_2
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))
⊢ ∃ i, p i ∧ 1 ∈ K i

pp: case refine_1.refine_3
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 y : G),
    x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) →
      y ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) → (∃ i, p i ∧ x ∈ K i) → (∃ i, p i ∧ y ∈ K i) → ∃ i, p i ∧ x * y ∈ K i

pp: case refine_1.refine_4
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 ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)), (∃ i, p i ∧ x ∈ K i) → ∃ i, p i ∧ x⁻¹ ∈ K i

Tactic:
·

Goal state after:
case refine_1.refine_2
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))
⊢ ∃ i, p i ∧ 1 ∈ K i
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_1.refine_3
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 y : G),
    x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) →
      y ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) → (∃ i, p i ∧ x ∈ K i) → (∃ i, p i ∧ y ∈ K i) → ∃ i, p i ∧ x * y ∈ K i

pp: case refine_1.refine_4
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 ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)), (∃ i, p i ∧ x ∈ K i) → ∃ i, p i ∧ x⁻¹ ∈ K i

Tactic:
·

Goal state after:
case refine_1.refine_3
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 y : G),
    x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) →
      y ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)) → (∃ i, p i ∧ x ∈ K i) → (∃ i, p i ∧ y ∈ K i) → ∃ i, p i ∧ x * y ∈ K i
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_1.refine_4
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 ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)), (∃ i, p i ∧ x ∈ K i) → ∃ i, p i ∧ x⁻¹ ∈ K i

Tactic:
·

Goal state after:
case refine_1.refine_4
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 ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i)), (∃ i, p i ∧ x ∈ K i) → ∃ i, p i ∧ x⁻¹ ∈ K i
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_2
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 ∧ x ∈ K i
i : ι
hi' : p i
hi : x ∈ K i
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i

Tactic:
·

Goal state after:
case refine_2
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 ∧ x ∈ K i
i : ι
hi' : p i
hi : x ∈ K i
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i
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 [Subgroup.comap_comap] using
      Subgroup.comap_mono (f := (f.symm : H →* G)) h

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

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
⊢ DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on fun i ↦ K i.down) {i | True}

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
⊢ PLift ι

Tactic:
·

Goal state after:
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
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
⊢ DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on fun i ↦ K i.down) {i | True}

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
⊢ PLift ι

Tactic:
·

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
⊢ DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on fun i ↦ K i.down) {i | True}
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : x / y ∈ f.ker
⊢ f x = f y

pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ x / y ∈ f.ker

Tactic:
·

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : x / y ∈ f.ker
⊢ f x = f y
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ x / y ∈ f.ker

Tactic:
·

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ x / y ∈ f.ker
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
⊢ PLift ι

Tactic:
·

Goal state after:
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
⊢ PLift ι
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ y⁻¹ * x ∈ f.ker

pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : y⁻¹ * x ∈ f.ker
⊢ f x = f y

Tactic:
·

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ y⁻¹ * x ∈ f.ker
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : y⁻¹ * x ∈ f.ker
⊢ f x = f y

Tactic:
·

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : y⁻¹ * x ∈ f.ker
⊢ f x = f y
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : G) (x : ι), a ∈ S x → ∀ (b : G) (x : ι), b ∈ S x → a * b = b * a

Tactic:
intro a i ha b j hb

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : G
i : ι
ha : a ∈ S i
b : G
j : ι
hb : b ∈ S j
⊢ a * b = b * a
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_1
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ ↑s ∪ ↑t, ∃ y ∈ s, ∃ z ∈ t, y * z = x

pp: case refine_2
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∃ y ∈ s, ∃ z ∈ t, y * z = 1

pp: case refine_3
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ (x y : C),
    x ∈ closure (↑s ∪ ↑t) →
      y ∈ closure (↑s ∪ ↑t) →
        (∃ y ∈ s, ∃ z ∈ t, y * z = x) → (∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y) → ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = x * y

pp: case refine_4
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ closure (↑s ∪ ↑t), (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹

Tactic:
·

Goal state after:
case refine_1
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ ↑s ∪ ↑t, ∃ y ∈ s, ∃ z ∈ t, y * z = x