Theorem: inversions_empty_iff_support_empty (Bruhat/Word.lean)

State before:
f : Equiv.Perm ℕ
⊢ Inversions f = ∅ ↔ support f = ∅
Tactic:
rw [← not_iff_not]
State after:
f : Equiv.Perm ℕ
⊢ ¬Inversions f = ∅ ↔ ¬support f = ∅

State before:
f : Equiv.Perm ℕ
⊢ ¬Inversions f = ∅ ↔ ¬support f = ∅
Tactic:
push_neg
State after:
f : Equiv.Perm ℕ
⊢ Set.Nonempty (Inversions f) ↔ Set.Nonempty (support f)

State before:
f : Equiv.Perm ℕ
⊢ Set.Nonempty (Inversions f) ↔ Set.Nonempty (support f)
Tactic:
constructor
State after:
case mp
f : Equiv.Perm ℕ
⊢ Set.Nonempty (Inversions f) → Set.Nonempty (support f)

case mpr
f : Equiv.Perm ℕ
⊢ Set.Nonempty (support f) → Set.Nonempty (Inversions f)

State before:
case mp
f : Equiv.Perm ℕ
⊢ Set.Nonempty (Inversions f) → Set.Nonempty (support f)

case mpr
f : Equiv.Perm ℕ
⊢ Set.Nonempty (support f) → Set.Nonempty (Inversions f)
Tactic:
. rintro ⟨⟨a, b⟩, hab⟩
  cases' mem_support_of_inversion _ _ _ hab with ha hb
  . exact ⟨_, ha⟩
  . exact ⟨_, hb⟩
State after:
case mpr
f : Equiv.Perm ℕ
⊢ Set.Nonempty (support f) → Set.Nonempty (Inversions f)

State before:
case mpr
f : Equiv.Perm ℕ
⊢ Set.Nonempty (support f) → Set.Nonempty (Inversions f)
Tactic:
. exact fun hf => ⟨_, min_support_mem_inversions f hf⟩
State after:
no goals

State before:
case mp
f : Equiv.Perm ℕ
⊢ Set.Nonempty (Inversions f) → Set.Nonempty (support f)
Tactic:
rintro ⟨⟨a, b⟩, hab⟩
State after:
case mp.intro.mk
f : Equiv.Perm ℕ
a b : ℕ
hab : (a, b) ∈ Inversions f
⊢ Set.Nonempty (support f)

State before:
case mp.intro.mk
f : Equiv.Perm ℕ
a b : ℕ
hab : (a, b) ∈ Inversions f
⊢ Set.Nonempty (support f)
Tactic:
cases' mem_support_of_inversion _ _ _ hab with ha hb
State after:
case mp.intro.mk.inl
f : Equiv.Perm ℕ
a b : ℕ
hab : (a, b) ∈ Inversions f
ha : a ∈ support f
⊢ Set.Nonempty (support f)

case mp.intro.mk.inr
f : Equiv.Perm ℕ
a b : ℕ
hab : (a, b) ∈ Inversions f
hb : b ∈ support f
⊢ Set.Nonempty (support f)

State before:
case mp.intro.mk.inl
f : Equiv.Perm ℕ
a b : ℕ
hab : (a, b) ∈ Inversions f
ha : a ∈ support f
⊢ Set.Nonempty (support f)

case mp.intro.mk.inr
f : Equiv.Perm ℕ
a b : ℕ
hab : (a, b) ∈ Inversions f
hb : b ∈ support f
⊢ Set.Nonempty (support f)
Tactic:
. exact ⟨_, ha⟩
State after:
case mp.intro.mk.inr
f : Equiv.Perm ℕ
a b : ℕ
hab : (a, b) ∈ Inversions f
hb : b ∈ support f
⊢ Set.Nonempty (support f)

State before:
case mp.intro.mk.inr
f : Equiv.Perm ℕ
a b : ℕ
hab : (a, b) ∈ Inversions f
hb : b ∈ support f
⊢ Set.Nonempty (support f)
Tactic:
. exact ⟨_, hb⟩
State after:
no goals

State before:
case mp.intro.mk.inl
f : Equiv.Perm ℕ
a b : ℕ
hab : (a, b) ∈ Inversions f
ha : a ∈ support f
⊢ Set.Nonempty (support f)
Tactic:
exact ⟨_, ha⟩
State after:
no goals

State before:
case mp.intro.mk.inr
f : Equiv.Perm ℕ
a b : ℕ
hab : (a, b) ∈ Inversions f
hb : b ∈ support f
⊢ Set.Nonempty (support f)
Tactic:
exact ⟨_, hb⟩
State after:
no goals

State before:
case mpr
f : Equiv.Perm ℕ
⊢ Set.Nonempty (support f) → Set.Nonempty (Inversions f)
Tactic:
exact fun hf => ⟨_, min_support_mem_inversions f hf⟩
State after:
no goals