Theorem: Subgroup.isMaximal_iff (Jordan/MaximalSubgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
K : Subgroup G
⊢ IsMaximal K ↔ K ≠ ⊤ ∧ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic:
constructor
State after:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
⊢ IsMaximal K → K ≠ ⊤ ∧ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤

case mpr
G : Type u_1
inst✝ : Group G
K : Subgroup G
⊢ (K ≠ ⊤ ∧ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤) → IsMaximal K

State before:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
⊢ IsMaximal K → K ≠ ⊤ ∧ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic:
intro hK
State after:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
⊢ K ≠ ⊤ ∧ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤

State before:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
⊢ K ≠ ⊤ ∧ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic:
constructor
State after:
case mp.left
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
⊢ K ≠ ⊤

case mp.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
⊢ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤

State before:
case mp.left
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
⊢ K ≠ ⊤
Tactic:
exact hK.ne_top
State after:
no goals

State before:
case mp.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
⊢ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic:
intro H g hKH hgK hgH
State after:
case mp.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ H = ⊤

State before:
case mp.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ H = ⊤
Tactic:
apply (isMaximal_def.1 hK).2
State after:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K < H

State before:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K < H
Tactic:
rw [← Ne.le_iff_lt]
State after:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K ≤ H

case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K ≠ H

State before:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K ≤ H

case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K ≠ H
Tactic:
exact hKH
State after:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K ≠ H

State before:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ K ≠ H
Tactic:
rw [Ne.def]
State after:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ ¬K = H

State before:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
⊢ ¬K = H
Tactic:
intro z
State after:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
z : K = H
⊢ False

State before:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ K
hgH : g ∈ H
z : K = H
⊢ False
Tactic:
rw [z] at hgK
State after:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ H
hgH : g ∈ H
z : K = H
⊢ False

State before:
case mp.right.a
G : Type u_1
inst✝ : Group G
K : Subgroup G
hK : IsMaximal K
H : Subgroup G
g : G
hKH : K ≤ H
hgK : g ∉ H
hgH : g ∈ H
z : K = H
⊢ False
Tactic:
exact hgK hgH
State after:
no goals

State before:
case mpr
G : Type u_1
inst✝ : Group G
K : Subgroup G
⊢ (K ≠ ⊤ ∧ ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤) → IsMaximal K
Tactic:
rintro ⟨hG, hmax⟩
State after:
case mpr.intro
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsMaximal K

State before:
case mpr.intro
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsMaximal K
Tactic:
constructor
State after:
case mpr.intro.out
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsCoatom K

State before:
case mpr.intro.out
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsCoatom K
Tactic:
constructor
State after:
case mpr.intro.out.left
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ K ≠ ⊤

case mpr.intro.out.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ ∀ (b : Subgroup G), K < b → b = ⊤

State before:
case mpr.intro.out.left
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ K ≠ ⊤
Tactic:
assumption
State after:
no goals

State before:
case mpr.intro.out.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ ∀ (b : Subgroup G), K < b → b = ⊤
Tactic:
intro H hKH
State after:
case mpr.intro.out.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
H : Subgroup G
hKH : K < H
⊢ H = ⊤

State before:
case mpr.intro.out.right
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
H : Subgroup G
hKH : K < H
⊢ H = ⊤
Tactic:
obtain ⟨g, hgH, hgK⟩ := Set.exists_of_ssubset hKH
State after:
case mpr.intro.out.right.intro.intro
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
H : Subgroup G
hKH : K < H
g : G
hgH : g ∈ ↑H
hgK : g ∉ ↑K
⊢ H = ⊤

State before:
case mpr.intro.out.right.intro.intro
G : Type u_1
inst✝ : Group G
K : Subgroup G
hG : K ≠ ⊤
hmax : ∀ (H : Subgroup G) (g : G), K ≤ H → g ∉ K → g ∈ H → H = ⊤
H : Subgroup G
hKH : K < H
g : G
hgH : g ∈ ↑H
hgK : g ∉ ↑K
⊢ H = ⊤
Tactic:
exact hmax H g (le_of_lt hKH) hgK hgH
State after:
no goals