Theorem: support_min_lt_apply (Bruhat/Word.lean)

State before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
have hg : ∃ n, f⁻¹ n ≠ n
State after:
case hg
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ ∃ n, f⁻¹ n ≠ n

f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)

State before:
case hg
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ ∃ n, f⁻¹ n ≠ n

f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
. simp_rw [ne_comm, ne_eq, Equiv.Perm.eq_inv_iff_eq]
  exact hf
State after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)

State before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
have hf_finv : ∀ n, f n ≠ n ↔ f⁻¹ n ≠ n
State after:
case hf_finv
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n

f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)

State before:
case hf_finv
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n

f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
. simp_rw [ne_comm, ne_eq, Equiv.Perm.eq_inv_iff_eq, eq_comm]
  exact fun n ↦ trivial
State after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)

State before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
have key : Nat.find hf = Nat.find hg
State after:
case key
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf = Nat.find hg

f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
⊢ Nat.find hf < f (Nat.find hf)

State before:
case key
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf = Nat.find hg

f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
. simp_rw [Nat.find_eq_iff, hf_finv, ← Nat.find_eq_iff hg]
State after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
⊢ Nat.find hf < f (Nat.find hf)

State before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
⊢ Nat.find hf < f (Nat.find hf)
Tactic:
rw [key]
State after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
⊢ Nat.find hg < f (Nat.find hg)

State before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
⊢ Nat.find hg < f (Nat.find hg)
Tactic:
have := support_min_lt_inv_apply f⁻¹ hg
State after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
this : Nat.find hg < f⁻¹⁻¹ (Nat.find hg)
⊢ Nat.find hg < f (Nat.find hg)

State before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
this : Nat.find hg < f⁻¹⁻¹ (Nat.find hg)
⊢ Nat.find hg < f (Nat.find hg)
Tactic:
rw [inv_inv] at this
State after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
this : Nat.find hg < f (Nat.find hg)
⊢ Nat.find hg < f (Nat.find hg)

State before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
key : Nat.find hf = Nat.find hg
this : Nat.find hg < f (Nat.find hg)
⊢ Nat.find hg < f (Nat.find hg)
Tactic:
exact this
State after:
no goals

State before:
case hg
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ ∃ n, f⁻¹ n ≠ n
Tactic:
simp_rw [ne_comm, ne_eq, Equiv.Perm.eq_inv_iff_eq]
State after:
case hg
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ ∃ n, ¬f n = n

State before:
case hg
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ ∃ n, ¬f n = n
Tactic:
exact hf
State after:
no goals

State before:
case hf_finv
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
Tactic:
simp_rw [ne_comm, ne_eq, Equiv.Perm.eq_inv_iff_eq, eq_comm]
State after:
case hf_finv
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ ℕ → True

State before:
case hf_finv
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
⊢ ℕ → True
Tactic:
exact fun n ↦ trivial
State after:
no goals

State before:
case key
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
hg : ∃ n, f⁻¹ n ≠ n
hf_finv : ∀ (n : ℕ), f n ≠ n ↔ f⁻¹ n ≠ n
⊢ Nat.find hf = Nat.find hg
Tactic:
simp_rw [Nat.find_eq_iff, hf_finv, ← Nat.find_eq_iff hg]
State after:
no goals