Theorem: exists_inversion_of_apply_lt (Bruhat/Word.lean)

State before:
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
⊢ ∃ m < n, (m, n) ∈ Inversions f
Tactic:
suffices : ∃ m < n, n ≤ f m
State after:
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
this : ∃ m < n, n ≤ f m
⊢ ∃ m < n, (m, n) ∈ Inversions f

case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
⊢ ∃ m < n, n ≤ f m

State before:
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
this : ∃ m < n, n ≤ f m
⊢ ∃ m < n, (m, n) ∈ Inversions f

case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
⊢ ∃ m < n, n ≤ f m
Tactic:
. obtain ⟨m, ⟨hmn, hm'⟩⟩ := this
  refine' ⟨m, hmn, _⟩
  simp [mem_inversions', hmn, (hn.trans_le hm').le]
State after:
case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
⊢ ∃ m < n, n ≤ f m

State before:
case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
⊢ ∃ m < n, n ≤ f m
Tactic:
by_contra! h_lt
State after:
case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
⊢ False

State before:
case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
⊢ False
Tactic:
have key1 : Finset.image f (Finset.range (n + 1)) ⊆ Finset.range n
State after:
case key1
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
⊢ Finset.image (⇑f) (Finset.range (n + 1)) ⊆ Finset.range n

case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
key1 : Finset.image (⇑f) (Finset.range (n + 1)) ⊆ Finset.range n
⊢ False

State before:
case key1
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
⊢ Finset.image (⇑f) (Finset.range (n + 1)) ⊆ Finset.range n

case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
key1 : Finset.image (⇑f) (Finset.range (n + 1)) ⊆ Finset.range n
⊢ False
Tactic:
. intro _ hm
  simp only [Finset.mem_image, Finset.mem_range] at hm ⊢
  obtain ⟨m', ⟨hm', rfl⟩⟩ := hm
  cases' Nat.lt_succ_iff_lt_or_eq.mp hm' with hm' hm'
  . exact h_lt _ hm'
  . simp [hm', hn]
State after:
case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
key1 : Finset.image (⇑f) (Finset.range (n + 1)) ⊆ Finset.range n
⊢ False

State before:
case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
key1 : Finset.image (⇑f) (Finset.range (n + 1)) ⊆ Finset.range n
⊢ False
Tactic:
replace key1 := Finset.card_le_card key1
State after:
case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
key1 : Finset.card (Finset.image (⇑f) (Finset.range (n + 1))) ≤ Finset.card (Finset.range n)
⊢ False

State before:
case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
key1 : Finset.card (Finset.image (⇑f) (Finset.range (n + 1))) ≤ Finset.card (Finset.range n)
⊢ False
Tactic:
simp [Finset.card_image_of_injective _ f.injective, Finset.card_range] at key1
State after:
no goals

State before:
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
this : ∃ m < n, n ≤ f m
⊢ ∃ m < n, (m, n) ∈ Inversions f
Tactic:
obtain ⟨m, ⟨hmn, hm'⟩⟩ := this
State after:
case intro.intro
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
m : ℕ
hmn : m < n
hm' : n ≤ f m
⊢ ∃ m < n, (m, n) ∈ Inversions f

State before:
case intro.intro
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
m : ℕ
hmn : m < n
hm' : n ≤ f m
⊢ ∃ m < n, (m, n) ∈ Inversions f
Tactic:
refine' ⟨m, hmn, _⟩
State after:
case intro.intro
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
m : ℕ
hmn : m < n
hm' : n ≤ f m
⊢ (m, n) ∈ Inversions f

State before:
case intro.intro
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
m : ℕ
hmn : m < n
hm' : n ≤ f m
⊢ (m, n) ∈ Inversions f
Tactic:
simp [mem_inversions', hmn, (hn.trans_le hm').le]
State after:
no goals

State before:
case key1
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
⊢ Finset.image (⇑f) (Finset.range (n + 1)) ⊆ Finset.range n
Tactic:
intro _ hm
State after:
case key1
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
a✝ : ℕ
hm : a✝ ∈ Finset.image (⇑f) (Finset.range (n + 1))
⊢ a✝ ∈ Finset.range n

State before:
case key1
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
a✝ : ℕ
hm : a✝ ∈ Finset.image (⇑f) (Finset.range (n + 1))
⊢ a✝ ∈ Finset.range n
Tactic:
simp only [Finset.mem_image, Finset.mem_range] at hm ⊢
State after:
case key1
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
a✝ : ℕ
hm : ∃ a < n + 1, f a = a✝
⊢ a✝ < n

State before:
case key1
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
a✝ : ℕ
hm : ∃ a < n + 1, f a = a✝
⊢ a✝ < n
Tactic:
obtain ⟨m', ⟨hm', rfl⟩⟩ := hm
State after:
case key1.intro.intro
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
m' : ℕ
hm' : m' < n + 1
⊢ f m' < n

State before:
case key1.intro.intro
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
m' : ℕ
hm' : m' < n + 1
⊢ f m' < n
Tactic:
cases' Nat.lt_succ_iff_lt_or_eq.mp hm' with hm' hm'
State after:
case key1.intro.intro.inl
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
m' : ℕ
hm'✝ : m' < n + 1
hm' : m' < n
⊢ f m' < n

case key1.intro.intro.inr
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
m' : ℕ
hm'✝ : m' < n + 1
hm' : m' = n
⊢ f m' < n

State before:
case key1.intro.intro.inl
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
m' : ℕ
hm'✝ : m' < n + 1
hm' : m' < n
⊢ f m' < n

case key1.intro.intro.inr
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
m' : ℕ
hm'✝ : m' < n + 1
hm' : m' = n
⊢ f m' < n
Tactic:
. exact h_lt _ hm'
State after:
case key1.intro.intro.inr
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
m' : ℕ
hm'✝ : m' < n + 1
hm' : m' = n
⊢ f m' < n

State before:
case key1.intro.intro.inr
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
m' : ℕ
hm'✝ : m' < n + 1
hm' : m' = n
⊢ f m' < n
Tactic:
. simp [hm', hn]
State after:
no goals

State before:
case key1.intro.intro.inl
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
m' : ℕ
hm'✝ : m' < n + 1
hm' : m' < n
⊢ f m' < n
Tactic:
exact h_lt _ hm'
State after:
no goals

State before:
case key1.intro.intro.inr
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
m' : ℕ
hm'✝ : m' < n + 1
hm' : m' = n
⊢ f m' < n
Tactic:
simp [hm', hn]
State after:
no goals