Theorem: support_min_lt_inv_apply (Bruhat/Word.lean)

State before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ Nat.find hf < f⁻¹ (Nat.find hf)
Tactic:
set n := Nat.find hf with hn
State after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
⊢ n < f⁻¹ n

State before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
⊢ n < f⁻¹ n
Tactic:
obtain ⟨hn', hn''⟩ := (Nat.find_eq_iff hf).mp hn.symm
State after:
case intro
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
hn' : f n ≠ n
hn'' : ∀ n_1 < n, ¬f n_1 ≠ n_1
⊢ n < f⁻¹ n

State before:
case intro
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
hn' : f n ≠ n
hn'' : ∀ n_1 < n, ¬f n_1 ≠ n_1
⊢ n < f⁻¹ n
Tactic:
specialize hn'' (f⁻¹ n)
State after:
case intro
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
hn' : f n ≠ n
hn'' : f⁻¹ n < n → ¬f (f⁻¹ n) ≠ f⁻¹ n
⊢ n < f⁻¹ n

State before:
case intro
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
hn' : f n ≠ n
hn'' : f⁻¹ n < n → ¬f (f⁻¹ n) ≠ f⁻¹ n
⊢ n < f⁻¹ n
Tactic:
rw [imp_not_comm, not_lt, f.apply_inv_self] at hn''
State after:
case intro
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
hn' : f n ≠ n
hn'' : n ≠ f⁻¹ n → n ≤ f⁻¹ n
⊢ n < f⁻¹ n

State before:
case intro
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
hn' : f n ≠ n
hn'' : n ≠ f⁻¹ n → n ≤ f⁻¹ n
⊢ n < f⁻¹ n
Tactic:
rw [ne_eq, ← Equiv.Perm.eq_inv_iff_eq] at hn'
State after:
case intro
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
hn' : ¬n = f⁻¹ n
hn'' : n ≠ f⁻¹ n → n ≤ f⁻¹ n
⊢ n < f⁻¹ n

State before:
case intro
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
hn' : ¬n = f⁻¹ n
hn'' : n ≠ f⁻¹ n → n ≤ f⁻¹ n
⊢ n < f⁻¹ n
Tactic:
apply lt_of_le_of_ne (hn'' hn') hn'
State after:
no goals