-- Mathlib/GroupTheory/Perm/Sign.lean
theorem mclosure_swap_castSucc_succ (n : ℕ) :
    Submonoid.closure (Set.range fun i : Fin n ↦ swap i.castSucc i.succ) = ⊤

Proof state:
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
lt : i < j
⊢ swap i j ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

Tactic:
induction' j using Fin.induction with j ih

Result:
case zero
n : ℕ
i : Fin (n + 1)
ne : i ≠ 0
lt : i < 0
⊢ swap i 0 ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

case succ
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
ne : i ≠ j.succ
lt : i < j.succ
⊢ swap i j.succ ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

Proof state:
case zero
n : ℕ
i : Fin (n + 1)
ne : i ≠ 0
lt : i < 0
⊢ swap i 0 ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

Tactic:
cases lt

Result:
no goals

Proof state:
case succ.inr
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
ne : i ≠ j.succ
lt : i < j.succ
mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ)
lts : i < j.castSucc
⊢ swap i j.succ ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

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

Result:
case succ.inr
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
ne : i ≠ j.succ
lt : i < j.succ
mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i => swap i.castSucc i.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 => swap i.castSucc i.succ))

Proof state:
case h
n : ℕ
⊢ {σ | σ.IsSwap} ⊆ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

Tactic:
rintro _ ⟨i, j, ne, rfl⟩

Result:
case h.intro.intro.intro
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
⊢ swap i j ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

Proof state:
case h.intro.intro.intro.inr
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this :
  ∀ (i j : Fin (n + 1)), i ≠ j → i < j → swap i j ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
lt : ¬i < j
⊢ swap j i ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

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

Result:
no goals

Proof state:
case h
n : ℕ
⊢ ⊤ ≤ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ)

Tactic:
rw [← mclosure_isSwap, Submonoid.closure_le]

Result:
case h
n : ℕ
⊢ {σ | σ.IsSwap} ⊆ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

Proof state:
case succ.inr
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
ne : i ≠ j.succ
lt : i < j.succ
mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i => swap i.castSucc i.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 => swap i.castSucc i.succ))

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

Result:
no goals

Proof state:
case h.intro.intro.intro
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
⊢ swap i j ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

Tactic:
wlog lt : i < j generalizing i j

Result:
case h.intro.intro.intro.inr
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this :
  ∀ (i j : Fin (n + 1)), i ≠ j → i < j → swap i j ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
lt : ¬i < j
⊢ swap i j ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
lt : i < j
⊢ swap i j ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

Proof state:
n : ℕ
⊢ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ) = ⊤

Tactic:
apply top_unique

Result:
case h
n : ℕ
⊢ ⊤ ≤ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ)

Proof state:
case succ
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
ne : i ≠ j.succ
lt : i < j.succ
mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ)
⊢ swap i j.succ ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

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

Result:
case succ.inl
n : ℕ
j : Fin n
mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ)
ih :
  j.castSucc ≠ j.castSucc →
    j.castSucc < j.castSucc →
      swap j.castSucc j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
ne : j.castSucc ≠ j.succ
lt : j.castSucc < j.succ
⊢ swap j.castSucc j.succ ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

case succ.inr
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
ne : i ≠ j.succ
lt : i < j.succ
mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ)
lts : i < j.castSucc
⊢ swap i j.succ ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

Proof state:
case h.intro.intro.intro.inr
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this :
  ∀ (i j : Fin (n + 1)), i ≠ j → i < j → swap i j ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
lt : ¬i < j
⊢ swap i j ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

Tactic:
rw [swap_comm]

Result:
case h.intro.intro.intro.inr
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this :
  ∀ (i j : Fin (n + 1)), i ≠ j → i < j → swap i j ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
lt : ¬i < j
⊢ swap j i ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

Proof state:
case succ.inl
n : ℕ
j : Fin n
mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ)
ih :
  j.castSucc ≠ j.castSucc →
    j.castSucc < j.castSucc →
      swap j.castSucc j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
ne : j.castSucc ≠ j.succ
lt : j.castSucc < j.succ
⊢ swap j.castSucc j.succ ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))

Tactic:
exact mem

Result:
no goals

Proof state:
case succ
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
ne : i ≠ j.succ
lt : i < j.succ
⊢ swap i j.succ ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.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⟩

Result:
case succ
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
ne : i ≠ j.succ
lt : i < j.succ
mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ)
⊢ swap i j.succ ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))