internlm/Lean-Github huggingface dataset:
Theorem: repbleByWord_aux
Proof state before:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : b = a
⊢ b ∈ s
Tactic:
subst b
Proof state after:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hb : a ∈ support g
⊢ a ∈ s
Theorem: repbleByWord_aux
Proof state before:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hb : a ∈ support g
⊢ a ∈ s
Tactic:
absurd (unswap_support f a)
Proof state after:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hb : a ∈ support g
⊢ a ∈ support (Equiv.swap a (f a) * f)
Theorem: repbleByWord_aux
Proof state before:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hb : a ∈ support g
⊢ a ∈ support (Equiv.swap a (f a) * f)
Tactic:
exact hb
Proof state after:
no goals
Theorem: repbleByWord
Proof state before:
f : Equiv.Perm ℕ
hf : Set.Finite (support f)
⊢ RepbleByWord f
Tactic:
exact repbleByWord_aux _ hf f (subset_refl _)
Proof state after:
no goals
Theorem: mem_inversions
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
p : α × α
⊢ p ∈ Inversions g ↔ (p.1 < p.2 ↔ g p.2 ≤ g p.1)
Tactic:
rfl
Proof state after:
no goals
Theorem: mem_inversions'
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a, b) ∈ Inversions g ↔ (a < b ↔ g b ≤ g a)
Tactic:
rfl
Proof state after:
no goals
Theorem: not_mem_inversions_diag
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a : α
⊢ (a, a) ∉ Inversions g
Tactic:
simp [mem_inversions']
Proof state after:
no goals
Theorem: mem_inversions_symm
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a, b) ∈ Inversions g ↔ (b, a) ∈ Inversions g
Tactic:
simp only [mem_inversions']
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Theorem: mem_inversions_symm
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
wlog h : a < b
Proof state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Theorem: mem_inversions_symm
Proof state before:
case inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
. cases' eq_or_lt_of_le (le_of_not_lt h) with h' h'
  . simp [h']
  . rw [this _ _ _ h']
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Theorem: mem_inversions_symm
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
have h' : g a ≠ g b := fun hg => h.ne (g.injective hg)
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a < b
h' : g a ≠ g b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Theorem: mem_inversions_symm
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a < b
h' : g a ≠ g b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
simp [h, h.not_lt, h'.symm.le_iff_lt]
Proof state after:
no goals
Theorem: mem_inversions_symm
Proof state before:
case inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
cases' eq_or_lt_of_le (le_of_not_lt h) with h' h'
Proof state after:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b = a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b < a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Theorem: mem_inversions_symm
Proof state before:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b = a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b < a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
. simp [h']
Proof state after:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b < a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Theorem: mem_inversions_symm
Proof state before:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b < a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
. rw [this _ _ _ h']
Proof state after:
no goals
Theorem: mem_inversions_symm
Proof state before:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b = a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
simp [h']
Proof state after:
no goals
Theorem: mem_inversions_symm
Proof state before:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b < a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
rw [this _ _ _ h']
Proof state after:
no goals
Theorem: mem_support_of_inversion
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : (a, b) ∈ Inversions g
⊢ a ∈ support g ∨ b ∈ support g
Tactic:
simp only [mem_inversions', support, ne_eq, Set.mem_setOf_eq] at hab ⊢
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a < b ↔ g b ≤ g a
⊢ ¬g a = a ∨ ¬g b = b
Theorem: mem_support_of_inversion
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a < b ↔ g b ≤ g a
⊢ ¬g a = a ∨ ¬g b = b
Tactic:
by_contra! hab'
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a < b ↔ g b ≤ g a
hab' : g a = a ∧ g b = b
⊢ False
Theorem: mem_support_of_inversion
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a < b ↔ g b ≤ g a
hab' : g a = a ∧ g b = b
⊢ False
Tactic:
rw [hab'.1, hab'.2, ← not_le] at hab
Proof state after:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : ¬b ≤ a ↔ b ≤ a
hab' : g a = a ∧ g b = b
⊢ False
Theorem: mem_support_of_inversion
Proof state before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : ¬b ≤ a ↔ b ≤ a
hab' : g a = a ∧ g b = b
⊢ False
Tactic:
exact not_iff_self hab
Proof state after:
no goals
Theorem: min_support_mem_inversions
Proof state before:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
⊢ (Nat.find hf, f⁻¹ (Nat.find hf)) ∈ Inversions f
Tactic:
rw [mem_inversions']
Proof 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)
Theorem: min_support_mem_inversions
Proof 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]
Proof state after:
no goals
Theorem: exists_inversion_of_apply_lt
Proof state before:
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
⊢ ∃ m < n, (m, n) ∈ Inversions f
Tactic:
suffices : ∃ m < n, n ≤ f m
Proof 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
Theorem: exists_inversion_of_apply_lt
Proof 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]
Proof state after:
case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
⊢ ∃ m < n, n ≤ f m
Theorem: exists_inversion_of_apply_lt
Proof state before:
case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
⊢ ∃ m < n, n ≤ f m
Tactic:
by_contra! h_lt
Proof state after:
case this
f : Equiv.Perm ℕ
n : ℕ
hn : f n < n
h_lt : ∀ m < n, f m < n
⊢ False
Theorem: exists_inversion_of_apply_lt
Proof 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
Proof 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
Theorem: exists_inversion_of_apply_lt
Proof 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]
Proof 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
Theorem: exists_inversion_of_apply_lt
Proof 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
Proof 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
Theorem: exists_inversion_of_apply_lt
Proof 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
Proof state after:
no goals
Theorem: exists_inversion_of_apply_lt
Proof 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
Proof 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
Theorem: exists_inversion_of_apply_lt
Proof 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, _⟩
Proof 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
Theorem: exists_inversion_of_apply_lt
Proof 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]
Proof state after:
no goals
Theorem: exists_inversion_of_apply_lt
Proof 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
Proof 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
Theorem: exists_inversion_of_apply_lt
Proof 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 ⊢
Proof 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
Theorem: exists_inversion_of_apply_lt
Proof 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
Proof 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
Theorem: exists_inversion_of_apply_lt
Proof 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'
Proof 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
Theorem: exists_inversion_of_apply_lt
Proof 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'
Proof 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
Theorem: exists_inversion_of_apply_lt
Proof 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]
Proof state after:
no goals
Theorem: exists_inversion_of_apply_lt
Proof 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'
Proof state after:
no goals
Theorem: exists_inversion_of_apply_lt
Proof 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]
Proof state after:
no goals
Theorem: inversions_empty_iff_support_empty
Proof state before:
f : Equiv.Perm ℕ
⊢ Inversions f = ∅ ↔ support f = ∅
Tactic:
rw [← not_iff_not]
Proof state after:
f : Equiv.Perm ℕ
⊢ ¬Inversions f = ∅ ↔ ¬support f = ∅
Theorem: inversions_empty_iff_support_empty
Proof state before:
f : Equiv.Perm ℕ
⊢ ¬Inversions f = ∅ ↔ ¬support f = ∅
Tactic:
push_neg
Proof state after:
f : Equiv.Perm ℕ
⊢ Set.Nonempty (Inversions f) ↔ Set.Nonempty (support f)
Theorem: inversions_empty_iff_support_empty
Proof state before:
f : Equiv.Perm ℕ
⊢ Set.Nonempty (Inversions f) ↔ Set.Nonempty (support f)
Tactic:
constructor
Proof 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)
Theorem: inversions_empty_iff_support_empty
Proof 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⟩
Proof state after:
case mpr
f : Equiv.Perm ℕ
⊢ Set.Nonempty (support f) → Set.Nonempty (Inversions f)
Theorem: inversions_empty_iff_support_empty
Proof 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⟩
Proof state after:
no goals
Theorem: inversions_empty_iff_support_empty
Proof state before:
case mp
f : Equiv.Perm ℕ
⊢ Set.Nonempty (Inversions f) → Set.Nonempty (support f)
Tactic:
rintro ⟨⟨a, b⟩, hab⟩
Proof state after:
case mp.intro.mk
f : Equiv.Perm ℕ
a b : ℕ
hab : (a, b) ∈ Inversions f
⊢ Set.Nonempty (support f)
Theorem: inversions_empty_iff_support_empty
Proof 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
Proof 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)
Theorem: inversions_empty_iff_support_empty
Proof 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⟩
Proof 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)
Theorem: inversions_empty_iff_support_empty
Proof 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⟩
Proof state after:
no goals
Theorem: inversions_empty_iff_support_empty
Proof 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⟩
Proof state after:
no goals
Theorem: inversions_empty_iff_support_empty
Proof 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⟩
Proof state after:
no goals
Theorem: inversions_empty_iff_support_empty
Proof 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⟩
Proof state after:
no goals
Theorem: inversions_comp
Proof state before:
f g : Equiv.Perm ℕ
⊢ Inversions (f * g) = (⇑(Equiv.prodCongr g g) ⁻¹' Inversions f) ∆ Inversions g
Tactic:
ext ⟨a, b⟩
Proof state after:
case h.mk
f g : Equiv.Perm ℕ
a b : ℕ
⊢ (a, b) ∈ Inversions (f * g) ↔ (a, b) ∈ (⇑(Equiv.prodCongr g g) ⁻¹' Inversions f) ∆ Inversions g
Theorem: inversions_comp
Proof state before:
case h.mk
f g : Equiv.Perm ℕ
a b : ℕ
⊢ (a, b) ∈ Inversions (f * g) ↔ (a, b) ∈ (⇑(Equiv.prodCongr g g) ⁻¹' Inversions f) ∆ Inversions g
Tactic:
simp only [Set.mem_symmDiff, Set.mem_preimage, Equiv.prodCongr_apply, Prod.map]
Proof state after:
case h.mk
f g : Equiv.Perm ℕ
a b : ℕ
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Theorem: inversions_comp
Proof state before:
case h.mk
f g : Equiv.Perm ℕ
a b : ℕ
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
wlog h : a < b
Proof state after:
case h.mk.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Theorem: inversions_comp
Proof state before:
case h.mk.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
. cases' (le_of_not_lt h).eq_or_lt with h' h'
  . simp [h', not_mem_inversions_diag]
  . repeat simp_rw [mem_inversions_symm _ a b, mem_inversions_symm _ (g a) (g b)]
    exact this f g _ _ h'
Proof state after:
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Theorem: inversions_comp
Proof state before:
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
cases' lt_or_le (g a) (g b) with hgab hgba
Proof state after:
case inl
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgab : g a < g b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

case inr
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgba : g b ≤ g a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Theorem: inversions_comp
Proof state before:
case inl
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgab : g a < g b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

case inr
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgba : g b ≤ g a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
. simp [mem_inversions', Set.mem_symmDiff, h, hgab, hgab.not_le]
Proof state after:
case inr
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgba : g b ≤ g a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Theorem: inversions_comp
Proof state before:
case inr
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgba : g b ≤ g a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
. simp [mem_inversions', Set.mem_symmDiff, h, hgba, hgba.not_lt]
Proof state after:
no goals