Theorem: MulAction.aux_lt_iff_lt_or_eq (Jordan/MultipleTransitivity.lean)

State before:
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
⊢ m < n - 1 ∨ m = n - 1
Tactic:
rw [Nat.lt_iff_le_not_le]
State after:
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m ∨ m = n - 1

State before:
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m ∨ m = n - 1
Tactic:
cases' dec_em (m = n - 1) with h h'
State after:
case inl
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h : m = n - 1
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m ∨ m = n - 1

case inr
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m ∨ m = n - 1

State before:
case inl
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h : m = n - 1
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m ∨ m = n - 1
Tactic:
exact Or.intro_right _ h
State after:
no goals

State before:
case inr
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m ∨ m = n - 1
Tactic:
apply Or.intro_left
State after:
case inr.h
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m

State before:
case inr.h
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ m ≤ n - 1 ∧ ¬n - 1 ≤ m
Tactic:
apply And.intro
State after:
case inr.h.left
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ m ≤ n - 1

case inr.h.right
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ ¬n - 1 ≤ m

State before:
case inr.h.left
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ m ≤ n - 1
Tactic:
exact Nat.le_pred_of_lt hmn
State after:
no goals

State before:
case inr.h.right
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
⊢ ¬n - 1 ≤ m
Tactic:
intro h
State after:
case inr.h.right
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
h : n - 1 ≤ m
⊢ False

State before:
case inr.h.right
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
h : n - 1 ≤ m
⊢ False
Tactic:
apply h'
State after:
case inr.h.right
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
h : n - 1 ≤ m
⊢ m = n - 1

State before:
case inr.h.right
M : Type ?u.247599
α : Type ?u.247602
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
m n : ℕ
hmn : m < n
h' : ¬m = n - 1
h : n - 1 ≤ m
⊢ m = n - 1
Tactic:
exact Nat.le_antisymm (Nat.le_pred_of_lt hmn) h
State after:
no goals