internlm/Lean-Github huggingface dataset:
Theorem: Finperm.closure_adjSwaps_eq
Proof state before:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
⊢ f ∈ Subgroup.closure adjSwaps ↔ f ∈ ⊤
Tactic:
simp only [Subgroup.mem_top, iff_true]
Proof state after:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
⊢ f ∈ Subgroup.closure adjSwaps
Theorem: Finperm.closure_adjSwaps_eq
Proof state before:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
⊢ f ∈ Subgroup.closure adjSwaps
Tactic:
have hss : (f.support : Set ℕ) ⊆ Set.Iic f.ub
Proof state after:
case hss
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
⊢ ↑f.support ⊆ Set.Iic (ub f)

case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
⊢ f ∈ Subgroup.closure adjSwaps
Theorem: Finperm.closure_adjSwaps_eq
Proof state before:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
⊢ f ∈ Subgroup.closure adjSwaps
Tactic:
have hf := restrict_mono hss <| mem_restrict_support f
Proof state after:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ restrict (Set.Iic (ub f))
⊢ f ∈ Subgroup.closure adjSwaps
Theorem: Finperm.closure_adjSwaps_eq
Proof state before:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ restrict (Set.Iic (ub f))
⊢ f ∈ Subgroup.closure adjSwaps
Tactic:
rw [← closure_adjSwapsBelow_eq] at hf
Proof state after:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ Subgroup.closure (adjSwapsBelow (ub f))
⊢ f ∈ Subgroup.closure adjSwaps
Theorem: Finperm.closure_adjSwaps_eq
Proof state before:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ Subgroup.closure (adjSwapsBelow (ub f))
⊢ f ∈ Subgroup.closure adjSwaps
Tactic:
refine (Subgroup.closure_mono ?_) hf
Proof state after:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ Subgroup.closure (adjSwapsBelow (ub f))
⊢ adjSwapsBelow (ub f) ⊆ adjSwaps
Theorem: Finperm.closure_adjSwaps_eq
Proof state before:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ Subgroup.closure (adjSwapsBelow (ub f))
⊢ adjSwapsBelow (ub f) ⊆ adjSwaps
Tactic:
rintro _ ⟨i, -, rfl⟩
Proof state after:
case h.intro.intro
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ Subgroup.closure (adjSwapsBelow (ub f))
i : ℕ
⊢ (fun i => swap i (i + 1)) i ∈ adjSwaps
Theorem: Finperm.closure_adjSwaps_eq
Proof state before:
case h.intro.intro
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ Subgroup.closure (adjSwapsBelow (ub f))
i : ℕ
⊢ (fun i => swap i (i + 1)) i ∈ adjSwaps
Tactic:
exact ⟨i, rfl⟩
Proof state after:
no goals
Theorem: Finperm.closure_adjSwaps_eq
Proof state before:
case hss
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
⊢ ↑f.support ⊆ Set.Iic (ub f)
Tactic:
exact fun x hx ↦ (f.lt_ub hx).le
Proof state after:
no goals
Theorem: Equiv.Perm.not_mem_support'
Proof state before:
α : Type u_1
x y : α
f✝ f : Perm α
⊢ x ∉ support' f ↔ f x = x
Tactic:
simp [support']
Proof state after:
no goals
Theorem: Equiv.Perm.mem_support'
Proof state before:
α : Type u_1
x y : α
f✝ f : Perm α
⊢ x ∈ support' f ↔ f x ≠ x
Tactic:
simp [support']
Proof state after:
no goals
Theorem: Equiv.Perm.support'_one
Proof state before:
α✝ : Type u_1
x y : α✝
f : Perm α✝
α : Type u_2
⊢ support' 1 = ∅
Tactic:
ext
Proof state after:
case h
α✝ : Type u_1
x y : α✝
f : Perm α✝
α : Type u_2
x✝ : α
⊢ x✝ ∈ support' 1 ↔ x✝ ∈ ∅
Theorem: Equiv.Perm.support'_one
Proof state before:
case h
α✝ : Type u_1
x y : α✝
f : Perm α✝
α : Type u_2
x✝ : α
⊢ x✝ ∈ support' 1 ↔ x✝ ∈ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: Equiv.Perm.support'_eq_empty
Proof state before:
α : Type u_1
x y : α
f✝ f : Perm α
⊢ support' f = ∅ ↔ f = 1
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.symm ▸ support'_one α⟩
Proof state after:
α : Type u_1
x y : α
f✝ f : Perm α
h : support' f = ∅
⊢ f = 1
Theorem: Equiv.Perm.support'_eq_empty
Proof state before:
α : Type u_1
x y : α
f✝ f : Perm α
h : support' f = ∅
⊢ f = 1
Tactic:
ext x
Proof state after:
case H
α : Type u_1
x✝ y : α
f✝ f : Perm α
h : support' f = ∅
x : α
⊢ f x = 1 x
Theorem: Equiv.Perm.support'_eq_empty
Proof state before:
case H
α : Type u_1
x✝ y : α
f✝ f : Perm α
h : support' f = ∅
x : α
⊢ f x = 1 x
Tactic:
simp only [support', ne_eq, eq_empty_iff_forall_not_mem, mem_setOf_eq, not_not] at h
Proof state after:
case H
α : Type u_1
x✝ y : α
f✝ f : Perm α
x : α
h : ∀ (x : α), f x = x
⊢ f x = 1 x
Theorem: Equiv.Perm.support'_eq_empty
Proof state before:
case H
α : Type u_1
x✝ y : α
f✝ f : Perm α
x : α
h : ∀ (x : α), f x = x
⊢ f x = 1 x
Tactic:
exact h x
Proof state after:
no goals
Theorem: Equiv.Perm.support'_ne_singleton
Proof state before:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
⊢ support' f ≠ {a}
Tactic:
intro h
Proof state after:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : support' f = {a}
⊢ False
Theorem: Equiv.Perm.support'_ne_singleton
Proof state before:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : support' f = {a}
⊢ False
Tactic:
simp only [Set.ext_iff, mem_support', ne_eq, mem_singleton_iff] at h
Proof state after:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : ∀ (x : α), ¬f x = x ↔ x = a
⊢ False
Theorem: Equiv.Perm.support'_ne_singleton
Proof state before:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : ∀ (x : α), ¬f x = x ↔ x = a
⊢ False
Tactic:
specialize h (f.symm a)
Proof state after:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : ¬f (f.symm a) = f.symm a ↔ f.symm a = a
⊢ False
Theorem: Equiv.Perm.support'_ne_singleton
Proof state before:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : ¬f (f.symm a) = f.symm a ↔ f.symm a = a
⊢ False
Tactic:
rw [eq_comm] at h
Proof state after:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : ¬f.symm a = f (f.symm a) ↔ f.symm a = a
⊢ False
Theorem: Equiv.Perm.support'_ne_singleton
Proof state before:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : ¬f.symm a = f (f.symm a) ↔ f.symm a = a
⊢ False
Tactic:
simp only [apply_symm_apply, not_iff_self] at h
Proof state after:
no goals
Theorem: Equiv.Perm.exists_ne_of_mem_support'
Proof state before:
α : Type u_1
x y : α
f : Perm α
a : α
ha : a ∈ support' f
⊢ ∃ b ∈ support' f, b ≠ a
Tactic:
refine by_contra <| fun h ↦ support'_ne_singleton f a ?_
Proof state after:
α : Type u_1
x y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ¬∃ b ∈ support' f, b ≠ a
⊢ support' f = {a}
Theorem: Equiv.Perm.exists_ne_of_mem_support'
Proof state before:
α : Type u_1
x y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ¬∃ b ∈ support' f, b ≠ a
⊢ support' f = {a}
Tactic:
simp only [Set.ext_iff, mem_support', ne_eq, mem_singleton_iff]
Proof state after:
α : Type u_1
x y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ¬∃ b ∈ support' f, b ≠ a
⊢ ∀ (x : α), ¬f x = x ↔ x = a
Theorem: Equiv.Perm.exists_ne_of_mem_support'
Proof state before:
α : Type u_1
x y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ¬∃ b ∈ support' f, b ≠ a
⊢ ∀ (x : α), ¬f x = x ↔ x = a
Tactic:
simp only [mem_support', ne_eq, not_exists, not_and, not_not] at h
Proof state after:
α : Type u_1
x y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ∀ (x : α), ¬f x = x → x = a
⊢ ∀ (x : α), ¬f x = x ↔ x = a
Theorem: Equiv.Perm.exists_ne_of_mem_support'
Proof state before:
α : Type u_1
x y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ∀ (x : α), ¬f x = x → x = a
⊢ ∀ (x : α), ¬f x = x ↔ x = a
Tactic:
refine fun x ↦ ⟨fun h' ↦ h _ h', ?_⟩
Proof state after:
α : Type u_1
x✝ y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ∀ (x : α), ¬f x = x → x = a
x : α
⊢ x = a → ¬f x = x
Theorem: Equiv.Perm.exists_ne_of_mem_support'
Proof state before:
α : Type u_1
x✝ y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ∀ (x : α), ¬f x = x → x = a
x : α
⊢ x = a → ¬f x = x
Tactic:
rintro rfl
Proof state after:
α : Type u_1
x✝ y : α
f : Perm α
x : α
ha : x ∈ support' f
h : ∀ (x_1 : α), ¬f x_1 = x_1 → x_1 = x
⊢ ¬f x = x
Theorem: Equiv.Perm.exists_ne_of_mem_support'
Proof state before:
α : Type u_1
x✝ y : α
f : Perm α
x : α
ha : x ∈ support' f
h : ∀ (x_1 : α), ¬f x_1 = x_1 → x_1 = x
⊢ ¬f x = x
Tactic:
exact ha
Proof state after:
no goals
Theorem: Equiv.Perm.support'_inv
Proof state before:
α : Type u_1
x y : α
f✝ f : Perm α
⊢ support' f⁻¹ = support' f
Tactic:
ext x
Proof state after:
case h
α : Type u_1
x✝ y : α
f✝ f : Perm α
x : α
⊢ x ∈ support' f⁻¹ ↔ x ∈ support' f
Theorem: Equiv.Perm.support'_inv
Proof state before:
case h
α : Type u_1
x✝ y : α
f✝ f : Perm α
x : α
⊢ x ∈ support' f⁻¹ ↔ x ∈ support' f
Tactic:
rw [mem_support', ne_eq, mem_support', inv_eq_iff_eq, eq_comm]
Proof state after:
no goals
Theorem: Equiv.Perm.support'_prod
Proof state before:
α : Type u_1
x y : α
f✝ f g : Perm α
⊢ support' (f * g) ⊆ support' f ∪ support' g
Tactic:
refine fun x hx ↦ by_contra <| fun h ↦ hx ?_
Proof state after:
α : Type u_1
x✝ y : α
f✝ f g : Perm α
x : α
hx : x ∈ support' (f * g)
h : x ∉ support' f ∪ support' g
⊢ (f * g) x = x
Theorem: Equiv.Perm.support'_prod
Proof state before:
α : Type u_1
x✝ y : α
f✝ f g : Perm α
x : α
hx : x ∈ support' (f * g)
h : x ∉ support' f ∪ support' g
⊢ (f * g) x = x
Tactic:
simp only [mem_union, not_or, not_mem_support'] at h
Proof state after:
α : Type u_1
x✝ y : α
f✝ f g : Perm α
x : α
hx : x ∈ support' (f * g)
h : f x = x ∧ g x = x
⊢ (f * g) x = x
Theorem: Equiv.Perm.support'_prod
Proof state before:
α : Type u_1
x✝ y : α
f✝ f g : Perm α
x : α
hx : x ∈ support' (f * g)
h : f x = x ∧ g x = x
⊢ (f * g) x = x
Tactic:
rw [coe_mul, Function.comp_apply]
Proof state after:
α : Type u_1
x✝ y : α
f✝ f g : Perm α
x : α
hx : x ∈ support' (f * g)
h : f x = x ∧ g x = x
⊢ f (g x) = x
Theorem: Equiv.Perm.support'_prod
Proof state before:
α : Type u_1
x✝ y : α
f✝ f g : Perm α
x : α
hx : x ∈ support' (f * g)
h : f x = x ∧ g x = x
⊢ f (g x) = x
Tactic:
simp [h.1, h.2]
Proof state after:
no goals
Theorem: Equiv.Perm.support'_swap
Proof state before:
α : Type u_1
x y : α
f : Perm α
inst✝ : DecidableEq α
hxy : x ≠ y
⊢ support' (swap x y) = {x, y}
Tactic:
ext z
Proof state after:
case h
α : Type u_1
x y : α
f : Perm α
inst✝ : DecidableEq α
hxy : x ≠ y
z : α
⊢ z ∈ support' (swap x y) ↔ z ∈ {x, y}
Theorem: Equiv.Perm.support'_swap
Proof state before:
case h
α : Type u_1
x y : α
f : Perm α
inst✝ : DecidableEq α
hxy : x ≠ y
z : α
⊢ z ∈ support' (swap x y) ↔ z ∈ {x, y}
Tactic:
simp only [support', ne_eq, mem_setOf_eq, mem_insert_iff, mem_singleton_iff]
Proof state after:
case h
α : Type u_1
x y : α
f : Perm α
inst✝ : DecidableEq α
hxy : x ≠ y
z : α
⊢ ¬(swap x y) z = z ↔ z = x ∨ z = y
Theorem: Equiv.Perm.support'_swap
Proof state before:
case h
α : Type u_1
x y : α
f : Perm α
inst✝ : DecidableEq α
hxy : x ≠ y
z : α
⊢ ¬(swap x y) z = z ↔ z = x ∨ z = y
Tactic:
rw [← Ne.def, Equiv.swap_apply_ne_self_iff, and_iff_right hxy]
Proof state after:
no goals
Theorem: Equiv.Perm.exists_pair_of_isSwap
Proof state before:
α : Type u_1
x y : α
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
hf : IsSwap f
⊢ ∃ p, f = swap p.lo p.hi
Tactic:
obtain ⟨x,y, hxy, rfl⟩ := hf
Proof state after:
case intro.intro.intro
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
⊢ ∃ p, swap x y = swap p.lo p.hi
Theorem: Equiv.Perm.exists_pair_of_isSwap
Proof state before:
case intro.intro.intro
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
⊢ ∃ p, swap x y = swap p.lo p.hi
Tactic:
obtain (h | h) := hxy.lt_or_lt
Proof state after:
case intro.intro.intro.inl
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h : x < y
⊢ ∃ p, swap x y = swap p.lo p.hi

case intro.intro.intro.inr
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h : y < x
⊢ ∃ p, swap x y = swap p.lo p.hi
Theorem: Equiv.Perm.exists_pair_of_isSwap
Proof state before:
case intro.intro.intro.inr
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h : y < x
⊢ ∃ p, swap x y = swap p.lo p.hi
Tactic:
rw [Equiv.swap_comm]
Proof state after:
case intro.intro.intro.inr
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h : y < x
⊢ ∃ p, swap y x = swap p.lo p.hi
Theorem: Equiv.Perm.exists_pair_of_isSwap
Proof state before:
case intro.intro.intro.inr
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h : y < x
⊢ ∃ p, swap y x = swap p.lo p.hi
Tactic:
exact ⟨Pair.mk y x h, rfl⟩
Proof state after:
no goals
Theorem: Equiv.Perm.exists_pair_of_isSwap
Proof state before:
case intro.intro.intro.inl
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h : x < y
⊢ ∃ p, swap x y = swap p.lo p.hi
Tactic:
exact ⟨Pair.mk x y h, rfl⟩
Proof state after:
no goals
Theorem: Equiv.Perm.swap_eq_swap
Proof state before:
α : Type u_1
x✝ y✝ : α
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x x' y y' : α
⊢ swap x y = swap x' y' ↔ x = x' ∧ y = y' ∨ x = y' ∧ y = x'
Tactic:
sorry
Proof state after:
no goals
Theorem: WordForSwap_toPerm_succ
Proof state before:
i k : ℕ
⊢ Word.toPerm (WordForSwap i (k + 1)) =
    Equiv.swap (i + (k + 1)) (i + (k + 2)) * Word.toPerm (WordForSwap i k) * Equiv.swap (i + (k + 1)) (i + (k + 2))
Tactic:
simp [WordForSwap, Word.toPerm]
Proof state after:
i k : ℕ
⊢ Equiv.swap (i + k + 1) (i + k + 1 + 1) *
      (List.prod (List.map (fun i => Equiv.swap i (i + 1)) (WordForSwap i k)) *
        Equiv.swap (i + k + 1) (i + k + 1 + 1)) =
    Equiv.swap (i + (k + 1)) (i + (k + 2)) * List.prod (List.map (fun i => Equiv.swap i (i + 1)) (WordForSwap i k)) *
      Equiv.swap (i + (k + 1)) (i + (k + 2))
Theorem: WordForSwap_toPerm_succ
Proof state before:
i k : ℕ
⊢ Equiv.swap (i + k + 1) (i + k + 1 + 1) *
      (List.prod (List.map (fun i => Equiv.swap i (i + 1)) (WordForSwap i k)) *
        Equiv.swap (i + k + 1) (i + k + 1 + 1)) =
    Equiv.swap (i + (k + 1)) (i + (k + 2)) * List.prod (List.map (fun i => Equiv.swap i (i + 1)) (WordForSwap i k)) *
      Equiv.swap (i + (k + 1)) (i + (k + 2))
Tactic:
rfl
Proof state after:
no goals
Theorem: wordForSwap_eq_swap
Proof state before:
i k : ℕ
⊢ Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
Tactic:
induction' k with k ih
Proof state after:
case zero
i : ℕ
⊢ Word.toPerm (WordForSwap i Nat.zero) = Equiv.swap i (i + (Nat.zero + 1))

case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Word.toPerm (WordForSwap i (Nat.succ k)) = Equiv.swap i (i + (Nat.succ k + 1))
Theorem: wordForSwap_eq_swap
Proof state before:
case zero
i : ℕ
⊢ Word.toPerm (WordForSwap i Nat.zero) = Equiv.swap i (i + (Nat.zero + 1))

case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Word.toPerm (WordForSwap i (Nat.succ k)) = Equiv.swap i (i + (Nat.succ k + 1))
Tactic:
. simp only [Nat.zero_eq, add_zero, Equiv.swap_self]
  rfl
Proof state after:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Word.toPerm (WordForSwap i (Nat.succ k)) = Equiv.swap i (i + (Nat.succ k + 1))
Theorem: wordForSwap_eq_swap
Proof state before:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Word.toPerm (WordForSwap i (Nat.succ k)) = Equiv.swap i (i + (Nat.succ k + 1))
Tactic:
. rw [WordForSwap_toPerm_succ, ih]
  change _ * _ * (Equiv.swap _ _)⁻¹ = _
  rw [← Equiv.swap_apply_apply, Equiv.swap_apply_left,
      Equiv.swap_apply_of_ne_of_ne (by simp) (by simp)]
Proof state after:
no goals
Theorem: wordForSwap_eq_swap
Proof state before:
case zero
i : ℕ
⊢ Word.toPerm (WordForSwap i Nat.zero) = Equiv.swap i (i + (Nat.zero + 1))
Tactic:
simp only [Nat.zero_eq, add_zero, Equiv.swap_self]
Proof state after:
case zero
i : ℕ
⊢ Word.toPerm (WordForSwap i 0) = Equiv.swap i (i + (0 + 1))
Theorem: wordForSwap_eq_swap
Proof state before:
case zero
i : ℕ
⊢ Word.toPerm (WordForSwap i 0) = Equiv.swap i (i + (0 + 1))
Tactic:
rfl
Proof state after:
no goals
Theorem: wordForSwap_eq_swap
Proof state before:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Word.toPerm (WordForSwap i (Nat.succ k)) = Equiv.swap i (i + (Nat.succ k + 1))
Tactic:
rw [WordForSwap_toPerm_succ, ih]
Proof state after:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Equiv.swap (i + (k + 1)) (i + (k + 2)) * Equiv.swap i (i + (k + 1)) * Equiv.swap (i + (k + 1)) (i + (k + 2)) =
    Equiv.swap i (i + (Nat.succ k + 1))
Theorem: wordForSwap_eq_swap
Proof state before:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Equiv.swap (i + (k + 1)) (i + (k + 2)) * Equiv.swap i (i + (k + 1)) * Equiv.swap (i + (k + 1)) (i + (k + 2)) =
    Equiv.swap i (i + (Nat.succ k + 1))
Tactic:
change _ * _ * (Equiv.swap _ _)⁻¹ = _
Proof state after:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Equiv.swap (i + (k + 1)) (i + (k + 2)) * Equiv.swap i (i + (k + 1)) * (Equiv.swap (i + (k + 1)) (i + (k + 2)))⁻¹ =
    Equiv.swap i (i + (Nat.succ k + 1))
Theorem: wordForSwap_eq_swap
Proof state before:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Equiv.swap (i + (k + 1)) (i + (k + 2)) * Equiv.swap i (i + (k + 1)) * (Equiv.swap (i + (k + 1)) (i + (k + 2)))⁻¹ =
    Equiv.swap i (i + (Nat.succ k + 1))
Tactic:
rw [← Equiv.swap_apply_apply, Equiv.swap_apply_left,
    Equiv.swap_apply_of_ne_of_ne (by simp) (by simp)]
Proof state after:
no goals
Theorem: wordForSwap_eq_swap
Proof state before:
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ i ≠ i + (k + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: wordForSwap_eq_swap
Proof state before:
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ i ≠ i + (k + 2)
Tactic:
simp
Proof state after:
no goals
Theorem: Word_mul
Proof state before:
w v : Word
⊢ Word.toPerm (w ++ v) = Word.toPerm w * Word.toPerm v
Tactic:
simp only [Word.toPerm, FreeMonoid.ofList_append, map_mul, FreeMonoid.lift_ofList]
Proof state after:
no goals
Theorem: swapHasWord
Proof state before:
i j : ℕ
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
cases' le_or_lt i j with h h
Proof state after:
case inl
i j : ℕ
h : i ≤ j
⊢ RepbleByWord (Equiv.swap i j)

case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Theorem: swapHasWord
Proof state before:
case inl
i j : ℕ
h : i ≤ j
⊢ RepbleByWord (Equiv.swap i j)

case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
cases' h.eq_or_lt with h h
Proof state after:
case inl.inl
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ RepbleByWord (Equiv.swap i j)

case inl.inr
i j : ℕ
h✝ : i ≤ j
h : i < j
⊢ RepbleByWord (Equiv.swap i j)

case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Theorem: swapHasWord
Proof state before:
case inl.inl
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ RepbleByWord (Equiv.swap i j)

case inl.inr
i j : ℕ
h✝ : i ≤ j
h : i < j
⊢ RepbleByWord (Equiv.swap i j)

case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
. use []
  rw [idHasWord, h, Equiv.swap_self]
  rfl
Proof state after:
case inl.inr
i j : ℕ
h✝ : i ≤ j
h : i < j
⊢ RepbleByWord (Equiv.swap i j)

case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Theorem: swapHasWord
Proof state before:
case inl.inr
i j : ℕ
h✝ : i ≤ j
h : i < j
⊢ RepbleByWord (Equiv.swap i j)

case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
. obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h
  use WordForSwap i k
  rw [wordForSwap_eq_swap, add_assoc]
Proof state after:
case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Theorem: swapHasWord
Proof state before:
case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
. obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h
  use WordForSwap j k
  rw [wordForSwap_eq_swap, add_assoc, Equiv.swap_comm]
Proof state after:
no goals
Theorem: swapHasWord
Proof state before:
case inl.inl
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
use []
Proof state after:
case h
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ Word.toPerm [] = Equiv.swap i j
Theorem: swapHasWord
Proof state before:
case h
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ Word.toPerm [] = Equiv.swap i j
Tactic:
rw [idHasWord, h, Equiv.swap_self]
Proof state after:
case h
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ 1 = Equiv.refl ℕ
Theorem: swapHasWord
Proof state before:
case h
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ 1 = Equiv.refl ℕ
Tactic:
rfl
Proof state after:
no goals
Theorem: swapHasWord
Proof state before:
case inl.inr
i j : ℕ
h✝ : i ≤ j
h : i < j
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h
Proof state after:
case inl.inr.intro
i k : ℕ
h✝ : i ≤ i + k + 1
h : i < i + k + 1
⊢ RepbleByWord (Equiv.swap i (i + k + 1))
Theorem: swapHasWord
Proof state before:
case inl.inr.intro
i k : ℕ
h✝ : i ≤ i + k + 1
h : i < i + k + 1
⊢ RepbleByWord (Equiv.swap i (i + k + 1))
Tactic:
use WordForSwap i k
Proof state after:
case h
i k : ℕ
h✝ : i ≤ i + k + 1
h : i < i + k + 1
⊢ Word.toPerm (WordForSwap i k) = Equiv.swap i (i + k + 1)
Theorem: swapHasWord
Proof state before:
case h
i k : ℕ
h✝ : i ≤ i + k + 1
h : i < i + k + 1
⊢ Word.toPerm (WordForSwap i k) = Equiv.swap i (i + k + 1)
Tactic:
rw [wordForSwap_eq_swap, add_assoc]
Proof state after:
no goals
Theorem: swapHasWord
Proof state before:
case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h
Proof state after:
case inr.intro
j k : ℕ
h : j < j + k + 1
⊢ RepbleByWord (Equiv.swap (j + k + 1) j)
Theorem: swapHasWord
Proof state before:
case inr.intro
j k : ℕ
h : j < j + k + 1
⊢ RepbleByWord (Equiv.swap (j + k + 1) j)
Tactic:
use WordForSwap j k
Proof state after:
case h
j k : ℕ
h : j < j + k + 1
⊢ Word.toPerm (WordForSwap j k) = Equiv.swap (j + k + 1) j
Theorem: swapHasWord
Proof state before:
case h
j k : ℕ
h : j < j + k + 1
⊢ Word.toPerm (WordForSwap j k) = Equiv.swap (j + k + 1) j
Tactic:
rw [wordForSwap_eq_swap, add_assoc, Equiv.swap_comm]
Proof state after:
no goals
Theorem: support_inv
Proof state before:
α : Type u_1
f : Equiv.Perm α
⊢ support f = support f⁻¹
Tactic:
ext a
Proof state after:
case h
α : Type u_1
f : Equiv.Perm α
a : α
⊢ a ∈ support f ↔ a ∈ support f⁻¹
Theorem: support_inv
Proof state before:
case h
α : Type u_1
f : Equiv.Perm α
a : α
⊢ a ∈ support f ↔ a ∈ support f⁻¹
Tactic:
simp [support, not_iff_not]
Proof state after:
case h
α : Type u_1
f : Equiv.Perm α
a : α
⊢ f a = a ↔ f⁻¹ a = a
Theorem: support_inv
Proof state before:
case h
α : Type u_1
f : Equiv.Perm α
a : α
⊢ f a = a ↔ f⁻¹ a = a
Tactic:
rw [← Equiv.Perm.eq_inv_iff_eq, eq_comm]
Proof state after:
no goals
Theorem: support_min_lt_inv_apply
Proof 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
Proof state after:
f : Equiv.Perm ℕ
hf : ∃ n, f n ≠ n
n : ℕ := Nat.find hf
hn : n = Nat.find hf
⊢ n < f⁻¹ n
Theorem: support_min_lt_inv_apply
Proof 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
Proof 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
Theorem: support_min_lt_inv_apply
Proof 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)
Proof 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
Theorem: support_min_lt_inv_apply
Proof 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''
Proof 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