awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
e : Perm α
⊢ Eq (α := ℤˣ)
    (((sign : Perm (Option α) →* ℤˣ) : (a : Perm (Option α)) → ℤˣ)
        ((Equiv.symm decomposeOption : (a : Option α × Perm α) → Perm (Option α)) (none, e)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) e : ℤˣ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Option
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Eq.{u_1 + 1} (α := Finset (Perm (Option α))) univ (map (Equiv.toEmbedding (Equiv.symm Perm.decomposeOption)) univ)

Tactic:
(Finset.univ_map_equiv_to_embedding _).symm

Premises used: Finset.univ_map_equiv_to_embedding, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ : Perm α
h_1 : σ = τ ∨ σ = swap i j * τ
h : σ = swap i j * τ
rw : τ = swap i j * (swap i j * τ)
rw₁ rw₂ : τ = τ
⊢ τ = swap i j * σ

Tactic:
rw [h, swap_mul_self_mul]

Premises used: Equiv.swap_mul_self_mul
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ ∨ σ = swap i j * τ
hτυ : τ = υ ∨ τ = swap i j * υ
inl : ∀ (hστ : σ = τ), σ = υ ∨ σ = swap i j * υ
inr : ∀ (hστ : σ = swap i j * τ), σ = υ ∨ σ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ

Tactic:
rcases hστ with hστ | hστ
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hτυ : τ = υ ∨ τ = swap i j * υ
hστ : σ = τ
inl : ∀ (hτυ : τ = υ), σ = υ ∨ σ = swap i j * υ
inl₁ : ∀ (hτυ : τ = swap i j * υ), σ = υ ∨ σ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ

Tactic:
rcases hτυ with hτυ | hτυ
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hτυ : τ = υ ∨ τ = swap i j * υ
hστ : σ = swap i j * τ
inr : ∀ (hτυ : τ = υ), σ = υ ∨ σ = swap i j * υ
inr₁ : ∀ (hτυ : τ = swap i j * υ), σ = υ ∨ σ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ

Tactic:
rcases hτυ with hτυ | hτυ
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = swap i j * υ
inr : υ = υ ∨ υ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ

Tactic:
rw [hστ, hτυ, swap_mul_self_mul]

Premises used: Equiv.swap_mul_self_mul
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = swap i j * υ
inr : υ = υ ∨ υ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ

Tactic:
try rw [hστ, hτυ, swap_mul_self_mul]

Premises used: Equiv.swap_mul_self_mul
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ

Tactic:
simp [hστ, hτυ]
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ

Tactic:
simp [hστ, hτυ]
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ

Tactic:
simp [hστ, hτυ]
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = swap i j * υ
⊢ υ = υ ∨ υ = swap i j * υ

Tactic:
simp [hστ, hτυ]
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
x : α
rw : Eq (α := α) ((1 : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((List.prod [] : (a : α) → α) x : α) ((f : (a : α) → α) x : α)

Tactic:
rw [List.prod_nil]

Premises used: List.prod_nil
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
x : α
⊢ Eq (α := α) ((1 : (a : α) → α) x : α) ((f : (a : α) → α) x : α)

Tactic:
(Classical.not_not.1 (mt h List.not_mem_nil)).symm

Premises used: Classical.not_not, mt, Iff.mp, Eq.symm, List.not_mem_nil
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
x : α
⊢ Eq (α := α) ((1 : (a : α) → α) x : α) ((f : (a : α) → α) x : α)

Tactic:
exact (Classical.not_not.1 (mt h List.not_mem_nil)).symm

Premises used: Classical.not_not, mt, Iff.mp, Eq.symm, List.not_mem_nil
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
⊢ ∀ (g : Perm α), Membership.mem (γ := List (Perm α)) [] g → g.IsSwap

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h_1 : ∀ {x_1 : α}, (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = (f : (a : α) → α) x
y : α
hy : (f : (a : α) → α) y ≠ y
h : y = x
⊢ False

Tactic:
simp [h, hfx.symm] at hy

Premises used: Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
m : { l : List (Perm α) // l.prod = swap x ((f : (a : α) → α) x) * f ∧ ∀ g ∈ l, g.IsSwap } :=
  swapFactorsAux l (swap x ((f : (a : α) → α) x) * f) ⋯
rw : swap x ((f : (a : α) → α) x) * (↑m : List (Perm α)).prod = f
rw₁ : swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f) = f
rw₂ : swap x ((f : (a : α) → α) x) * swap x ((f : (a : α) → α) x) * f = f
rw₃ : Equiv.trans (swap x ((f : (a : α) → α) x)) (swap x ((f : (a : α) → α) x)) * f = f
rw₄ : Equiv.refl α * f = f
rw₅ : 1 * f = f
rw₆ rw₇ : f = f
⊢ (swap x ((f : (a : α) → α) x) :: (↑m : List (Perm α))).prod = f

Tactic:
rw [List.prod_cons, m.2.1, ← mul_assoc, mul_def (swap x (f x)), swap_swap, ← one_def,
          one_mul]

Premises used: Equiv.Perm.one_def, mul_assoc, Equiv.swap, Equiv.Perm.mul_def, And.left, List.prod_cons, DFunLike.coe, Equiv.swap_swap, one_mul, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
f : Perm α
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
intro : ∀ (val : Fintype α), motive f
⊢ motive f

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
f : Perm α
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val : Fintype α
intro : ∀ (l : List (Perm α)) (hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap), motive f
⊢ motive f

Tactic:
obtain ⟨l, hl⟩ := (truncSwapFactors f).out

Premises used: Equiv.Perm.truncSwapFactors, Trunc.out
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val : Fintype α
f : Perm α
hl : List.prod [] = f ∧ ∀ (g : Perm α), Membership.mem (γ := List (Perm α)) [] g → g.IsSwap
⊢ motive f

Tactic:
simp only [one, hl.left.symm, List.prod_nil]

Premises used: And.left, List.prod_nil, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val : Fintype α
g : Perm α
l : List (Perm α)
ih : ∀ (f : Perm α) (hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap), motive f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
⊢ g ∈ g :: l

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val : Fintype α
g : Perm α
l : List (Perm α)
ih : ∀ (f : Perm α) (hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap), motive f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
intro : ∀ (x y : α) (hxy : x ≠ y ∧ g = swap x y), motive f
⊢ motive f

Tactic:
rcases hl.2 g (by simp) with ⟨x, y, hxy⟩

Premises used: And.right
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val : Fintype α
g : Perm α
l : List (Perm α)
ih : ∀ (f : Perm α) (hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap), motive f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
x y : α
hxy : x ≠ y ∧ g = swap x y
intro : motive (swap x y * l.prod)
⊢ motive f

Tactic:
rw [← hl.1, List.prod_cons, hxy.2]

Premises used: And.right, And.left, List.prod_cons
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val : Fintype α
g : Perm α
l : List (Perm α)
ih : ∀ (f : Perm α) (hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap), motive f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
x y : α
hxy : x ≠ y ∧ g = swap x y
⊢ motive (swap x y * l.prod)

Tactic:
swap_mul _ _ _ hxy.1 (ih _ ⟨rfl, fun v hv => hl.2 _ (List.mem_cons_of_mem _ hv)⟩)

Premises used: List.mem_cons_of_mem, And.right, And.left, And.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val : Fintype α
g : Perm α
l : List (Perm α)
ih : ∀ (f : Perm α) (hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap), motive f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
x y : α
hxy : x ≠ y ∧ g = swap x y
⊢ motive (swap x y * l.prod)

Tactic:
exact swap_mul _ _ _ hxy.1 (ih _ ⟨rfl, fun v hv => hl.2 _ (List.mem_cons_of_mem _ hv)⟩)

Premises used: List.mem_cons_of_mem, And.right, And.left, And.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
f : Perm α
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val : Fintype α
l : List (Perm α)
hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap
intro :
  ∀ (f : Perm α) (hl : List.prod [] = f ∧ ∀ (g : Perm α), Membership.mem (γ := List (Perm α)) [] g → g.IsSwap), motive f
intro₁ :
  ∀ (g : Perm α) (l : List (Perm α)) (ih : ∀ (f : Perm α) (hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap), motive f) (f : Perm α)
    (hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap), motive f
⊢ motive f

Tactic:
induction l generalizing f with
  | nil =>
    simp only [one, hl.left.symm, List.prod_nil]
  | cons g l ih =>
    rcases hl.2 g (by simp) with ⟨x, y, hxy⟩
    rw [← hl.1, List.prod_cons, hxy.2]
    exact swap_mul _ _ _ hxy.1 (ih _ ⟨rfl, fun v hv => hl.2 _ (List.mem_cons_of_mem _ hv)⟩)

Premises used: Finset.cons, And.left, List.prod_nil, Eq.symm, List.prod_cons
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
intro : ∀ (val : Fintype α), Eq.{u + 1} (α := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap}) ⊤
⊢ Eq.{u + 1} (α := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap}) ⊤

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
val : Fintype α
⊢ Eq.{u + 1} (α := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap}) ⊤

Tactic:
top_unique fun x _ ↦ ?_

Premises used: top_unique
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
val : Fintype α
intro :
  ∀ (x : Perm α),
    Membership.mem (γ := Submonoid (Perm α)) ⊤ x →
      Membership.mem (γ := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap}) x
⊢ Eq.{u + 1} (α := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap}) ⊤

Tactic:
refine top_unique fun x _ ↦ ?_

Premises used: top_unique
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
val : Fintype α
x : Perm α
h : Membership.mem (γ := Submonoid (Perm α)) ⊤ x
⊢ (↑(Trunc.out x.truncSwapFactors) : List (Perm α)).prod = x

Tactic:
obtain ⟨h1, h2⟩ := (truncSwapFactors x).out.prop

Premises used: Equiv.Perm.truncSwapFactors, Subtype.prop, Trunc.out
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
val : Fintype α
x : Perm α
h : Membership.mem (γ := Submonoid (Perm α)) ⊤ x
h1 : (↑(Trunc.out x.truncSwapFactors) : List (Perm α)).prod = x
⊢ ∀ g ∈ (↑(Trunc.out x.truncSwapFactors) : List (Perm α)), g.IsSwap

Tactic:
obtain ⟨h1, h2⟩ := (truncSwapFactors x).out.prop

Premises used: Equiv.Perm.truncSwapFactors, Subtype.prop, Trunc.out
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
val : Fintype α
x : Perm α
h : Membership.mem (γ := Submonoid (Perm α)) ⊤ x
h1 : (↑(Trunc.out x.truncSwapFactors) : List (Perm α)).prod = x
h2 : ∀ g ∈ (↑(Trunc.out x.truncSwapFactors) : List (Perm α)), g.IsSwap
intro :
  Membership.mem (γ := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap})
    (↑(Trunc.out x.truncSwapFactors) : List (Perm α)).prod
⊢ Membership.mem (γ := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap}) x

Tactic:
rw [← h1]
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
val : Fintype α
x : Perm α
h : Membership.mem (γ := Submonoid (Perm α)) ⊤ x
h1 : (↑(Trunc.out x.truncSwapFactors) : List (Perm α)).prod = x
h2 : ∀ g ∈ (↑(Trunc.out x.truncSwapFactors) : List (Perm α)), g.IsSwap
⊢ Membership.mem (γ := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap})
    (↑(Trunc.out x.truncSwapFactors) : List (Perm α)).prod

Tactic:
Submonoid.list_prod_mem _ fun y hy ↦ Submonoid.subset_closure (h2 y hy)

Premises used: Set.Mem, Submonoid.list_prod_mem, Submonoid.subset_closure
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
val : Fintype α
x : Perm α
h : Membership.mem (γ := Submonoid (Perm α)) ⊤ x
h1 : (↑(Trunc.out x.truncSwapFactors) : List (Perm α)).prod = x
h2 : ∀ g ∈ (↑(Trunc.out x.truncSwapFactors) : List (Perm α)), g.IsSwap
⊢ Membership.mem (γ := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap})
    (↑(Trunc.out x.truncSwapFactors) : List (Perm α)).prod

Tactic:
exact Submonoid.list_prod_mem _ fun y hy ↦ Submonoid.subset_closure (h2 y hy)

Premises used: Submonoid.list_prod_mem, Submonoid.subset_closure
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
⊢ Eq.{u + 1} (α := Subgroup (Perm α)) (Subgroup.closure {σ : Perm α | σ.IsSwap}) ⊤

Tactic:
Subgroup.closure_eq_top_of_mclosure_eq_top mclosure_isSwap

Premises used: Subgroup.closure_eq_top_of_mclosure_eq_top, Equiv.Perm.mclosure_isSwap
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
h :
  LE.le (α := Submonoid (Perm (Fin (n + 1)))) ⊤ (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ))
⊢ Eq (α := Submonoid (Perm (Fin (n + 1)))) (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) ⊤

Tactic:
apply top_unique

Premises used: top_unique
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
h :
  {σ : Perm (Fin (n + 1)) | σ.IsSwap} ⊆
    (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
⊢ LE.le (α := Submonoid (Perm (Fin (n + 1)))) ⊤ (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ))

Tactic:
rw [← mclosure_isSwap, Submonoid.closure_le]

Premises used: Equiv.Perm.mclosure_isSwap, Submonoid.closure_le
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
h :
  ∀
    (this :
      ∀ (i j : Fin (n + 1)) (ne : i ≠ j) (lt : i < j),
        swap i j ∈
          (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1)))))
    (lt : ¬i < j),
    swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
wlog :
  ∀ (i j : Fin (n + 1)) (ne : i ≠ j) (lt : i < j),
    swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
⊢ swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))

Tactic:
wlog lt : i < j generalizing i j
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this :
  ∀ (i j : Fin (n + 1)) (ne : i ≠ j) (lt : i < j),
    swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
lt : ¬i < j
h : swap j i ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
⊢ swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))

Tactic:
rw [swap_comm]

Premises used: Equiv.swap_comm
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this :
  ∀ (i j : Fin (n + 1)) (ne : i ≠ j) (lt : i < j),
    swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
lt : ¬i < j
⊢ swap j i ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))

Tactic:
this _ _ ne.symm (ne.lt_or_gt.resolve_left lt)

Premises used: Or.resolve_left, Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this :
  ∀ (i j : Fin (n + 1)) (ne : i ≠ j) (lt : i < j),
    swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
lt : ¬i < j
⊢ swap j i ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))

Tactic:
exact this _ _ ne.symm (ne.lt_or_gt.resolve_left lt)

Premises used: Or.resolve_left, Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
i : Fin (n + 1)
ne : i ≠ 0
lt : i < 0
⊢ swap i 0 ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))

Tactic:
cases lt
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  ∀ (ne : i ≠ j.castSucc) (lt : i < j.castSucc),
    swap i j.castSucc ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
ne : i ≠ j.succ
lt : i < j.succ
⊢ Membership.mem (γ := Submonoid (Perm (Fin (n + 1))))
    (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) (swap j.castSucc j.succ)

Tactic:
have mem : swap j.castSucc j.succ ∈ Submonoid.closure
      (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ) := Submonoid.subset_closure ⟨_, rfl⟩
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  ∀ (ne : i ≠ j.castSucc) (lt : i < j.castSucc),
    swap i j.castSucc ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
ne : i ≠ j.succ
lt : i < j.succ
mem :
  Membership.mem (γ := Submonoid (Perm (Fin (n + 1))))
    (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) (swap j.castSucc j.succ)
succ :
  ∀
    (ih :
      ∀ (ne : j.castSucc ≠ j.castSucc) (lt : j.castSucc < j.castSucc),
        swap j.castSucc j.castSucc ∈
          (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1)))))
    (ne : j.castSucc ≠ j.succ) (lt : j.castSucc < j.succ),
    swap j.castSucc j.succ ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
succ₁ :
  ∀ (lts : i < j.castSucc),
    swap i j.succ ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
⊢ swap i j.succ ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))

Tactic:
obtain rfl | lts := (Fin.le_castSucc_iff.mpr lt).eq_or_lt

Premises used: Iff.mpr, LE.le.eq_or_lt, Fin.le_castSucc_iff, rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
j : Fin n
mem :
  Membership.mem (γ := Submonoid (Perm (Fin (n + 1))))
    (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) (swap j.castSucc j.succ)
ih :
  ∀ (ne : j.castSucc ≠ j.castSucc) (lt : j.castSucc < j.castSucc),
    swap j.castSucc j.castSucc ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
ne : j.castSucc ≠ j.succ
lt : j.castSucc < j.succ
⊢ swap j.castSucc j.succ ∈
    (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))

Tactic:
mem
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
j : Fin n
mem :
  Membership.mem (γ := Submonoid (Perm (Fin (n + 1))))
    (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) (swap j.castSucc j.succ)
ih :
  ∀ (ne : j.castSucc ≠ j.castSucc) (lt : j.castSucc < j.castSucc),
    swap j.castSucc j.castSucc ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
ne : j.castSucc ≠ j.succ
lt : j.castSucc < j.succ
⊢ swap j.castSucc j.succ ∈
    (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))

Tactic:
exact mem
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  ∀ (ne : i ≠ j.castSucc) (lt : i < j.castSucc),
    swap i j.castSucc ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
ne : i ≠ j.succ
lt : i < j.succ
mem :
  Membership.mem (γ := Submonoid (Perm (Fin (n + 1))))
    (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) (swap j.castSucc j.succ)
lts : i < j.castSucc
succ :
  swap j.castSucc j.succ * swap i j.castSucc * swap j.castSucc j.succ ∈
    (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
⊢ swap i j.succ ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))

Tactic:
rw [swap_comm, ← swap_mul_swap_mul_swap (y := Fin.castSucc j) lts.ne lt.ne]

Premises used: Equiv.swap_comm, Equiv.swap_mul_swap_mul_swap, LT.lt.ne
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  ∀ (ne : i ≠ j.castSucc) (lt : i < j.castSucc),
    swap i j.castSucc ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
ne : i ≠ j.succ
lt : i < j.succ
mem :
  Membership.mem (γ := Submonoid (Perm (Fin (n + 1))))
    (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) (swap j.castSucc j.succ)
lts : i < j.castSucc
⊢ swap j.castSucc j.succ * swap i j.castSucc * swap j.castSucc j.succ ∈
    (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))

Tactic:
mul_mem (mul_mem mem <| ih lts.ne lts) mem

Premises used: LT.lt.ne, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  ∀ (ne : i ≠ j.castSucc) (lt : i < j.castSucc),
    swap i j.castSucc ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
ne : i ≠ j.succ
lt : i < j.succ
mem :
  Membership.mem (γ := Submonoid (Perm (Fin (n + 1))))
    (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) (swap j.castSucc j.succ)
lts : i < j.castSucc
⊢ swap j.castSucc j.succ * swap i j.castSucc * swap j.castSucc j.succ ∈
    (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))

Tactic:
exact mul_mem (mul_mem mem <| ih lts.ne lts) mem

Premises used: LT.lt.ne, MulMemClass.mul_mem