mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α < 4
⊢ alternatingGroup α ≤ G

pp: case inr
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
⊢ alternatingGroup α ≤ G

Tactic:
·

Goal state after:
case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α < 4
⊢ alternatingGroup α ≤ G
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case pos
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
hn' : n ≤ Nat.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

pp: case neg
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
hn' : ¬n ≤ Nat.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
·

Goal state after:
case pos
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
hn' : n ≤ Nat.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case neg
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
hn' : ¬n ≤ Nat.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
·

Goal state after:
case neg
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
hn' : ¬n ≤ Nat.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inr.hsn
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ (↑g.support)ᶜ.ncard = n + 1

pp: case inr.hsn'
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ n + 2 < Nat.card α

pp: case inr.hprim
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)

Tactic:
·

Goal state after:
case inr.hsn
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ (↑g.support)ᶜ.ncard = n + 1
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inr.hsn'
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ n + 2 < Nat.card α

pp: case inr.hprim
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ IsPreprimitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)

Tactic:
·

Goal state after:
case inr.hsn'
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ n + 2 < Nat.card α
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case inl
α✝ : Type u_2
n : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * 0 ≤ Nat.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 0

pp: case inr
α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n

Tactic:
·

Goal state after:
case inl
α✝ : Type u_2
n : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * 0 ≤ Nat.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 0
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case inr.inl
α✝ : Type u_2
n : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * 1 ≤ Nat.card α
hn0 : 1 ≠ 0
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 1

pp: case inr.inr
α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n

Tactic:
·

Goal state after:
case inr.inl
α✝ : Type u_2
n : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * 1 ≤ Nat.card α
hn0 : 1 ≠ 0
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 1
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case h0
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ (↑s).Nonempty

pp: case h1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ (↑s)ᶜ.Nonempty

pp: case hs
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ Nat.card α ≠ 2 * (↑s).ncard

Tactic:
·

Goal state after:
case h0
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ (↑s).Nonempty
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ n

Tactic:
by lia

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
⊢ Nat.succ 1 ≠ 0

Tactic:
by lia

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case h1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ (↑s)ᶜ.Nonempty

pp: case hs
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ Nat.card α ≠ 2 * (↑s).ncard

Tactic:
·

Goal state after:
case h1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ (↑s)ᶜ.Nonempty
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case hs
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ Nat.card α ≠ 2 * (↑s).ncard

Tactic:
·

Goal state after:
case hs
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝ : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ Nat.card α ≠ 2 * (↑s).ncard
Module: Mathlib.GroupTheory.MonoidLocalization.Lemmas

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
N : ι → Type u_3
inst✝¹ : (i : ι) → CommMonoid (M i)
inst✝ : (i : ι) → CommMonoid (N i)
S : (i : ι) → Submonoid (M i)
f : (i : ι) → M i → N i
hf : ∀ (i : ι), (S i).IsLocalizationMap (f i)
x y : (i : ι) → M i
eq : Pi.map f x = Pi.map f y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
by
    choose c hc using fun i ↦ (hf i).exists_of_eq congr($eq i)
    exact ⟨⟨_, fun i _ ↦ (c i).2⟩, funext hc⟩

Goal state after:
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inl
G : Type u_1
inst✝ : Group G
H✝ : Subgroup G
hG : IsSimpleGroup G
H : Subgroup G
h_le : H ≤ ⊥
hSubn : ⊥.IsSubnormal
hN : (H.subgroupOf ⊥).Normal
Knorm : ⊥.Normal
⊢ H.Normal

pp: case step.inr
G : Type u_1
inst✝ : Group G
H✝ : Subgroup G
hG : IsSimpleGroup G
H : Subgroup G
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
Knorm : ⊤.Normal
⊢ H.Normal

Tactic:
·

Goal state after:
case step.inl
G : Type u_1
inst✝ : Group G
H✝ : Subgroup G
hG : IsSimpleGroup G
H : Subgroup G
h_le : H ≤ ⊥
hSubn : ⊥.IsSubnormal
hN : (H.subgroupOf ⊥).Normal
Knorm : ⊥.Normal
⊢ H.Normal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inr
G : Type u_1
inst✝ : Group G
H✝ : Subgroup G
hG : IsSimpleGroup G
H : Subgroup G
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
Knorm : ⊤.Normal
⊢ H.Normal

Tactic:
·

Goal state after:
case step.inr
G : Type u_1
inst✝ : Group G
H✝ : Subgroup G
hG : IsSimpleGroup G
H : Subgroup G
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
Knorm : ⊤.Normal
⊢ H.Normal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inl
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
HK : H ≤ ⊤
hS : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
⊢ H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

pp: case step.inr
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
K' : Subgroup G
HK' : K < K'
hS' : K'.IsSubnormal
hN' : (K.subgroupOf K').Normal
⊢ H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
·

Goal state after:
case step.inl
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
HK : H ≤ ⊤
hS : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
⊢ H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inl.inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
hS : ⊤.IsSubnormal
HK : ⊤ ≤ ⊤
hN : (⊤.subgroupOf ⊤).Normal
⊢ ⊤ = ⊤ ∨ ∃ K, ⊤ < K ∧ K.IsSubnormal ∧ (⊤.subgroupOf K).Normal

pp: case step.inl.inr
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
HK : H ≤ ⊤
hS : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
hH : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
·

Goal state after:
case step.inl.inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
hS : ⊤.IsSubnormal
HK : ⊤ ≤ ⊤
hN : (⊤.subgroupOf ⊤).Normal
⊢ ⊤ = ⊤ ∨ ∃ K, ⊤ < K ∧ K.IsSubnormal ∧ (⊤.subgroupOf K).Normal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inl.inr
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
HK : H ≤ ⊤
hS : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
hH : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
·

Goal state after:
case step.inl.inr
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
HK : H ≤ ⊤
hS : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
hH : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inr.inl
G : Type u_1
inst✝ : Group G
H✝ H K' : Subgroup G
hS' : K'.IsSubnormal
HK : H ≤ H
hS : H.IsSubnormal
hN : (H.subgroupOf H).Normal
HK' : H < K'
hN' : (H.subgroupOf K').Normal
⊢ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

pp: case step.inr.inr
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
K' : Subgroup G
HK' : K < K'
hS' : K'.IsSubnormal
hN' : (K.subgroupOf K').Normal
hH : H ≠ K
⊢ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
·

Goal state after:
case step.inr.inl
G : Type u_1
inst✝ : Group G
H✝ H K' : Subgroup G
hS' : K'.IsSubnormal
HK : H ≤ H
hS : H.IsSubnormal
hN : (H.subgroupOf H).Normal
HK' : H < K'
hN' : (H.subgroupOf K').Normal
⊢ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inr.inr
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
K' : Subgroup G
HK' : K < K'
hS' : K'.IsSubnormal
hN' : (K.subgroupOf K').Normal
hH : H ≠ K
⊢ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
·

Goal state after:
case step.inr.inr
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
K' : Subgroup G
HK' : K < K'
hS' : K'.IsSubnormal
hN' : (K.subgroupOf K').Normal
hH : H ≠ K
⊢ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B 1)
⊢ ↑((toSubgroupEquiv φ (-1)) ((toSubgroupEquiv φ 1) a)) = ↑a

pp: case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B (-1))
⊢ ↑((toSubgroupEquiv φ (- -1)) ((toSubgroupEquiv φ (-1)) a)) = ↑a

Tactic:
·

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B 1)
⊢ ↑((toSubgroupEquiv φ (-1)) ((toSubgroupEquiv φ 1) a)) = ↑a
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B (-1))
⊢ ↑((toSubgroupEquiv φ (- -1)) ((toSubgroupEquiv φ (-1)) a)) = ↑a

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B (-1))
⊢ ↑((toSubgroupEquiv φ (- -1)) ((toSubgroupEquiv φ (-1)) a)) = ↑a
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
⊢ ⊤.IsSubnormal

pp: case inr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
HK : H < K
Ksn : K.IsSubnormal
h : (H.subgroupOf K).Normal
⊢ H.IsSubnormal

Tactic:
·

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
⊢ ⊤.IsSubnormal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
HK : H < K
Ksn : K.IsSubnormal
h : (H.subgroupOf K).Normal
⊢ H.IsSubnormal

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
HK : H < K
Ksn : K.IsSubnormal
h : (H.subgroupOf K).Normal
⊢ H.IsSubnormal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inl
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
ne_top : H ≠ ⊤
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
ih : ⊤ ≠ ⊤ → ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

pp: case step.inr
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : K ≠ ⊤ → ∃ K_1, K_1.Normal ∧ K ≤ K_1 ∧ K_1 < ⊤
ne_top : H ≠ ⊤
K_ne : K ≠ ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
·

Goal state after:
case step.inl
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
ne_top : H ≠ ⊤
h_le : H ≤ ⊤
hSubn : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
ih : ⊤ ≠ ⊤ → ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inr
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : K ≠ ⊤ → ∃ K_1, K_1.Normal ∧ K ≤ K_1 ∧ K_1 < ⊤
ne_top : H ≠ ⊤
K_ne : K ≠ ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
·

Goal state after:
case step.inr
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : K ≠ ⊤ → ∃ K_1, K_1.Normal ∧ K ≤ K_1 ∧ K_1 < ⊤
ne_top : H ≠ ⊤
K_ne : K ≠ ⊤
⊢ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
hN : ⊤.IsSubnormal
⊢ ⊤ = ⊤ ∨ ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤

pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
hN : H.IsSubnormal
H_ne : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
·

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
hN : ⊤.IsSubnormal
⊢ ⊤ = ⊤ ∨ ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
hN : H.IsSubnormal
H_ne : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
hN : H.IsSubnormal
H_ne : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case right
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ (match 0 with
      | 0 => H
      | n.succ => f n) =
      H ∧
    (match n + 1 with
      | 0 => H
      | n.succ => f n) =
      ⊤

pp: case left
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ Monotone fun x ↦
    match x with
    | 0 => H
    | n.succ => f n

pp: case left
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ ∀ (i : ℕ),
    ((match i with
          | 0 => H
          | n.succ => f n).subgroupOf
        (match i + 1 with
        | 0 => H
        | n.succ => f n)).Normal

Tactic:
·

Goal state after:
case right
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ (match 0 with
      | 0 => H
      | n.succ => f n) =
      H ∧
    (match n + 1 with
      | 0 => H
      | n.succ => f n) =
      ⊤
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case left
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ Monotone fun x ↦
    match x with
    | 0 => H
    | n.succ => f n

pp: case left
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ ∀ (i : ℕ),
    ((match i with
          | 0 => H
          | n.succ => f n).subgroupOf
        (match i + 1 with
        | 0 => H
        | n.succ => f n)).Normal

Tactic:
·

Goal state after:
case left
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ Monotone fun x ↦
    match x with
    | 0 => H
    | n.succ => f n
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
g : G
w : NormalWord d
u' : ℤˣ
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
⊢ w.head ∈ d.set u'

pp: case inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
u' : ℤˣ
g' : G
h' : (u', g') ∈ w.toList
⊢ g' ∈ d.set u'

Tactic:
·

Goal state after:
case inl
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
g : G
w : NormalWord d
u' : ℤˣ
h1 : w.head ∈ d.set u'
h2 : ∀ u'_1 ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u' → u' = u'_1
⊢ w.head ∈ d.set u'
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
u' : ℤˣ
g' : G
h' : (u', g') ∈ w.toList
⊢ g' ∈ d.set u'

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
u' : ℤˣ
g' : G
h' : (u', g') ∈ w.toList
⊢ g' ∈ d.set u'
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case left
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ ∀ (i : ℕ),
    ((match i with
          | 0 => H
          | n.succ => f n).subgroupOf
        (match i + 1 with
        | 0 => H
        | n.succ => f n)).Normal

Tactic:
·

Goal state after:
case left
G : Type u_1
inst✝ : Group G
H✝ H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
n : ℕ
f : ℕ → Subgroup G
hf : Monotone f
f0 : ∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal
fn : f 0 = K ∧ f n = ⊤
⊢ ∀ (i : ℕ),
    ((match i with
          | 0 => H
          | n.succ => f n).subgroupOf
        (match i + 1 with
        | 0 => H
        | n.succ => f n)).Normal