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

Goal state before:
pp: case refine_2
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
s : Set G
n : G
h : n ∈ normalClosure s
g : G
⊢ g * 1 * g⁻¹ ∈ normalClosure s

pp: case refine_3
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
s : Set G
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * (x * y) * g⁻¹ ∈ normalClosure s

pp: case refine_4
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
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ g * x⁻¹ * g⁻¹ ∈ normalClosure s

Tactic:
·

Goal state after:
case refine_2
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
s : Set G
n : G
h : n ∈ normalClosure s
g : G
⊢ g * 1 * g⁻¹ ∈ normalClosure s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_3
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
s : Set G
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * (x * y) * g⁻¹ ∈ normalClosure s

pp: case refine_4
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
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ g * x⁻¹ * g⁻¹ ∈ normalClosure s

Tactic:
·

Goal state after:
case refine_3
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
s : Set G
n : G
h : n ∈ normalClosure s
g x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * (x * y) * g⁻¹ ∈ normalClosure s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_4
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
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ g * x⁻¹ * g⁻¹ ∈ normalClosure s

Tactic:
·

Goal state after:
case refine_4
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
s : Set G
n : G
h : n ∈ normalClosure s
g x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ g * x⁻¹ * g⁻¹ ∈ normalClosure s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
hx : x ∈ conjugatesOfSet s
⊢ x ∈ N

pp: case refine_2
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
⊢ 1 ∈ N

pp: case refine_3
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
ihy : y ∈ N
⊢ x * y ∈ N

pp: case refine_4
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
⊢ x⁻¹ ∈ N

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
hx : x ∈ conjugatesOfSet s
⊢ x ∈ N
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
⊢ 1 ∈ N

pp: case refine_3
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
ihy : y ∈ N
⊢ x * y ∈ N

pp: case refine_4
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
⊢ x⁻¹ ∈ N

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
⊢ 1 ∈ N
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_3
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
ihy : y ∈ N
⊢ x * y ∈ N

pp: case refine_4
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
⊢ x⁻¹ ∈ N

Tactic:
·

Goal state after:
case refine_3
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x y : G
x✝¹ : x ∈ closure (conjugatesOfSet s)
x✝ : y ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
ihy : y ∈ N
⊢ x * y ∈ N
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_4
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
⊢ x⁻¹ ∈ N

Tactic:
·

Goal state after:
case refine_4
G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
a : G
w : a ∈ normalClosure s
x : G
x✝ : x ∈ closure (conjugatesOfSet s)
ihx : x ∈ N
⊢ x⁻¹ ∈ N
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
g : G
⊢ H.normalCore ≤ map (↑(MulAut.conj g)) H

pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H.normalCore

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
g : G
⊢ H.normalCore ≤ map (↑(MulAut.conj g)) H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H.normalCore

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
⊢ ⨅ g, map (↑(MulAut.conj g)) H ≤ H.normalCore
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

pp: case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → (x • s ∩ t).Nonempty

Tactic:
·

Goal state after:
case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → (x • s ∩ t).Nonempty

Tactic:
·

Goal state after:
case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → (x • s ∩ t).Nonempty
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

pp: case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → (x • s ∩ t).Nonempty

Tactic:
·

Goal state after:
case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → (x • s ∩ t).Nonempty

Tactic:
·

Goal state after:
case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → (x • s ∩ t).Nonempty
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

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

pp: case inr
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
·

Goal state after:
case inl
α : Type u_2
inst✝ : Group α
s t : Set α
a b : α
hAB : a • s ∩ b • t = ∅
⊢ ∃ z, a • s ∩ b • t ⊆ z • (s⁻¹ * s ∩ (t⁻¹ * t))
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective ⇑(map f) → Function.Surjective f

pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective f → Function.Surjective ⇑(map f)

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective ⇑(map f) → Function.Surjective f
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) ≤ normalClosure (⇑f '' s)

pp: case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ normalClosure (⇑f '' s) ≤ map f (normalClosure s)

Tactic:
·

Goal state after:
case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) ≤ normalClosure (⇑f '' s)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ normalClosure (⇑f '' s) ≤ map f (normalClosure s)

Tactic:
·

Goal state after:
case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ normalClosure (⇑f '' s) ≤ map f (normalClosure s)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons.inl
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : f i < g i
⊢ f i * (map f l).prod < g i * (map g l).prod

pp: case cons.inr
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : ∃ a, a ∈ l ∧ f a < g a
⊢ f i * (map f l).prod < g i * (map g l).prod

Tactic:
·

Goal state after:
case cons.inl
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : f i < g i
⊢ f i * (map f l).prod < g i * (map g l).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons.inr
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : ∃ a, a ∈ l ∧ f a < g a
⊢ f i * (map f l).prod < g i * (map g l).prod

Tactic:
·

Goal state after:
case cons.inr
ι : Type u_1
M : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Preorder M
inst✝³ : MulLeftStrictMono M
inst✝² : MulLeftMono M
inst✝¹ : MulRightStrictMono M
inst✝ : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : (∀ (i : ι), i ∈ l → f i ≤ g i) → (∃ i, i ∈ l ∧ f i < g i) → (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h✝ : ∃ a, a ∈ l ∧ f a < g a
⊢ f i * (map f l).prod < g i * (map g l).prod
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y * x⁻¹ * y⁻¹ = 1
⊢ x * y = y * x

Tactic:
·

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y * x⁻¹ * y⁻¹ = 1
⊢ x * y = y * x
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case left
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₁.toSubmonoid

pp: case right
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₂.toSubmonoid

Tactic:
·

Goal state after:
case left
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₁.toSubmonoid
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ f i✝ ≤ max (f i✝) (g i✝)

pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ g i✝ ≤ max (f i✝) (g i✝)

Tactic:
·

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ f i✝ ≤ max (f i✝) (g i✝)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ g i✝ ≤ max (f i✝) (g i✝)

Tactic:
·

Goal state after:
case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
i✝ : α
a✝ : i✝ ∈ l
⊢ g i✝ ≤ max (f i✝) (g i✝)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case right
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₂.toSubmonoid

Tactic:
·

Goal state after:
case right
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₂.toSubmonoid
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ min (f i✝) (g i✝) ≤ f i✝

pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ min (f i✝) (g i✝) ≤ g i✝

Tactic:
·

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ min (f i✝) (g i✝) ≤ f i✝
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ min (f i✝) (g i✝) ≤ g i✝

Tactic:
·

Goal state after:
case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ min (f i✝) (g i✝) ≤ g i✝
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ min (map f l).prod (map g l).prod

Tactic:
rw [le_min_iff]
  constructor <;> apply List.prod_le_prod' <;> intros
  · apply min_le_left
  · apply min_le_right

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

Goal state before:
pp: case inl
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
⊢ (take n L).prod ≤ (take (n + 1) L).prod

pp: case inr
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : L.length ≤ n
⊢ (take n L).prod ≤ (take (n + 1) L).prod

Tactic:
·

Goal state after:
case inl
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
⊢ (take n L).prod ≤ (take (n + 1) L).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case inr
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : L.length ≤ n
⊢ (take n L).prod ≤ (take (n + 1) L).prod

Tactic:
·

Goal state after:
case inr
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : L.length ≤ n
⊢ (take n L).prod ≤ (take (n + 1) L).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons.inl
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
⊢ x ≤ (x :: ys).prod

pp: case cons.inr
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x ∈ ys
⊢ x ≤ (y :: ys).prod

Tactic:
·

Goal state after:
case cons.inl
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
⊢ x ≤ (x :: ys).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons.inr
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x ∈ ys
⊢ x ≤ (y :: ys).prod

Tactic:
·

Goal state after:
case cons.inr
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x ∈ ys
⊢ x ≤ (y :: ys).prod
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ c⁻¹ * x * c ∈ N

pp: case refine_2
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h) ⟨c⁻¹ * x * c, ?refine_1⟩ = ⟨x, hx⟩

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ c⁻¹ * x * c ∈ N
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ normalClosure {⟨c * g * c⁻¹, hg'⟩} = ⊤

Tactic:
rw [eq_top_iff, ← MonoidHom.range_eq_top.2 hs, MonoidHom.range_eq_map]

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ map (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h) ⊤ ≤ normalClosure {⟨c * g * c⁻¹, hg'⟩}
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case pos
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : l = []
⊢ f (a * l.prod) ≤ f a * (map f l).prod

pp: case neg
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
⊢ f (a * l.prod) ≤ f a * (map f l).prod

Tactic:
·

Goal state after:
case pos
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : l = []
⊢ f (a * l.prod) ≤ f a * (map f l).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.List

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

Tactic:
simp [h_mul]

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

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r s a b → r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

pp: case mpr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ (r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd) → Lex r s a b

Tactic:
·

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r s a b → r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd