Theorem: min_support_mem_inversions (Bruhat/Word.lean)

State before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ (Nat.find hf, f⁻¹ (Nat.find hf)) ∈ Inversions f
Tactic:
rw [mem_inversions']
State after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ Nat.find hf < f⁻¹ (Nat.find hf) ↔ f (f⁻¹ (Nat.find hf)) ≤ f (Nat.find hf)

State before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ Nat.find hf < f⁻¹ (Nat.find hf) ↔ f (f⁻¹ (Nat.find hf)) ≤ f (Nat.find hf)
Tactic:
simp only [support_min_lt_inv_apply f hf, Equiv.Perm.apply_inv_self,
           (support_min_lt_apply f hf).le]
State after:
no goals