Theorem: subgroup_of_group_of_order_two (Jordan/PermMaximal.lean)

State before:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : Fintype.card ↥H ≤ 1
⊢ H = ⊥ ∨ H = ⊤
Tactic:
apply Or.intro_left
State after:
case inl.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : Fintype.card ↥H ≤ 1
⊢ H = ⊥

State before:
case inl.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : Fintype.card ↥H ≤ 1
⊢ H = ⊥
Tactic:
apply Subgroup.eq_bot_of_card_le
State after:
case inl.h.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : Fintype.card ↥H ≤ 1
⊢ Fintype.card ↥H ≤ 1

State before:
case inl.h.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : Fintype.card ↥H ≤ 1
⊢ Fintype.card ↥H ≤ 1
Tactic:
exact h
State after:
no goals

State before:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ H = ⊥ ∨ H = ⊤
Tactic:
apply Or.intro_right
State after:
case inr.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ H = ⊤

State before:
case inr.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ H = ⊤
Tactic:
apply Subgroup.eq_top_of_card_eq
State after:
case inr.h.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H = Fintype.card G

State before:
case inr.h.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H = Fintype.card G
Tactic:
apply le_antisymm
State after:
case inr.h.h.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H ≤ Fintype.card G

case inr.h.h.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card G ≤ Fintype.card ↥H

State before:
case inr.h.h.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H ≤ Fintype.card G
Tactic:
apply Nat.le_of_dvd
State after:
case inr.h.h.a.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ 0 < Fintype.card G

case inr.h.h.a.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H ∣ Fintype.card G

State before:
case inr.h.h.a.h
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ 0 < Fintype.card G

case inr.h.h.a.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H ∣ Fintype.card G
Tactic:
refine' Fintype.card_pos
State after:
case inr.h.h.a.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H ∣ Fintype.card G

State before:
case inr.h.h.a.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card ↥H ∣ Fintype.card G
Tactic:
refine' Subgroup.card_subgroup_dvd_card H
State after:
no goals

State before:
case inr.h.h.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ Fintype.card G ≤ Fintype.card ↥H
Tactic:
rw [hG]
State after:
case inr.h.h.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ 2 ≤ Fintype.card ↥H

State before:
case inr.h.h.a
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
hG : Fintype.card G = 2
H : Subgroup G
h : 1 < Fintype.card ↥H
⊢ 2 ≤ Fintype.card ↥H
Tactic:
exact h
State after:
no goals