Theorem: alternatingGroup.three_le (Jordan/AlternatingMaximal.lean)

State before:
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
⊢ 3 ≤ c
Tactic:
cases' Nat.eq_or_lt_of_le h with h h
State after:
case inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
h : 1 = n
⊢ 3 ≤ c

case inr
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
h : 1 < n
⊢ 3 ≤ c

State before:
case inr
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
h : 1 < n
⊢ 3 ≤ c
Tactic:
rw [Nat.succ_le_iff]
State after:
case inr
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
h : 1 < n
⊢ 2 < c

State before:
case inr
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
h : 1 < n
⊢ 2 < c
Tactic:
exact lt_of_le_of_lt h h'
State after:
no goals

State before:
case inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : n < c
hh' : c ≠ 2 * n
h : 1 = n
⊢ 3 ≤ c
Tactic:
rw [← h] at h' hh'
State after:
case inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
⊢ 3 ≤ c

State before:
case inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h' : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
⊢ 3 ≤ c
Tactic:
cases' Nat.eq_or_lt_of_le h' with h' h'
State after:
case inl.inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h'✝ : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
h' : Nat.succ 1 = c
⊢ 3 ≤ c

case inl.inr
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h'✝ : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
h' : Nat.succ 1 < c
⊢ 3 ≤ c

State before:
case inl.inr
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h'✝ : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
h' : Nat.succ 1 < c
⊢ 3 ≤ c
Tactic:
exact h'
State after:
no goals

State before:
case inl.inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h'✝ : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
h' : Nat.succ 1 = c
⊢ 3 ≤ c
Tactic:
exfalso
State after:
case inl.inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h'✝ : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
h' : Nat.succ 1 = c
⊢ False

State before:
case inl.inl
α : Type ?u.123292
inst✝¹ : Fintype α
inst✝ : DecidableEq α
c n : ℕ
h✝ : 1 ≤ n
h'✝ : 1 < c
hh' : c ≠ 2 * 1
h : 1 = n
h' : Nat.succ 1 = c
⊢ False
Tactic:
apply hh' h'.symm
State after:
no goals