-- Mathlib/GroupTheory/Perm/Sign.lean
theorem swap_induction_on [Finite α] {P : Perm α → Prop} (f : Perm α) :
    P 1 → (∀ f x y, x ≠ y → P f → P (swap x y * f)) → P f

Proof state:
case intro.mk.cons
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
⊢ P f

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

Result:
case intro.mk.cons.intro.intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
x y : α
hxy : x ≠ y ∧ g = swap x y
⊢ P f

Proof state:
case intro.mk.cons
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f

Tactic:
intro h1 hmul_swap

Result:
case intro.mk.cons
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
⊢ P f

Proof state:
case intro.mk
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f : Perm α
val✝ : Fintype α
l : List (Perm α)
hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f

Tactic:
induction' l with g l ih generalizing f

Result:
case intro.mk.nil
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
val✝ : Fintype α
f : Perm α
hl : [].prod = f ∧ ∀ g ∈ [], g.IsSwap
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f

case intro.mk.cons
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f

Proof state:
case intro.mk.cons.intro.intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
x y : α
hxy : x ≠ y ∧ g = swap x y
⊢ P (swap x y * l.prod)

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

Result:
no goals

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
⊢ g ∈ g :: l

Tactic:
simp

Result:
no goals

Proof state:
case intro.mk.nil
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
val✝ : Fintype α
f : Perm α
hl : [].prod = f ∧ ∀ g ∈ [], g.IsSwap
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f

Tactic:
simp +contextual only [hl.left.symm, List.prod_nil, forall_true_iff]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f : Perm α
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f : Perm α
val✝ : Fintype α
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f

Proof state:
case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f : Perm α
val✝ : Fintype α
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f

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

Result:
case intro.mk
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f : Perm α
val✝ : Fintype α
l : List (Perm α)
hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f

Proof state:
case intro.mk.cons.intro.intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
x y : α
hxy : x ≠ y ∧ g = swap x y
⊢ P f

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

Result:
case intro.mk.cons.intro.intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
x y : α
hxy : x ≠ y ∧ g = swap x y
⊢ P (swap x y * l.prod)