case intro
α : Type u
β : Type v
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
α : Type u
β : Type v
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
cases nonempty_fintype α
case intro.mk
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f : Perm α
val✝ : Fintype α
l : List (Perm α)
hl : List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
case intro
α : Type u
β : Type v
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
cases' (truncSwapFactors f).out with l hl
case intro.mk.nil
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l : List (Perm α)
hl✝ : List.prod l = f✝ ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
f : Perm α
hl : List.prod [] = f ∧ ∀ (g : Perm α), g ∈ [] → IsSwap g
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f

case intro.mk.cons
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
case intro.mk
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f : Perm α
val✝ : Fintype α
l : List (Perm α)
hl : List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
induction' l with g l ih generalizing f
no goals
case intro.mk.nil
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l : List (Perm α)
hl✝ : List.prod l = f✝ ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
f : Perm α
hl : List.prod [] = f ∧ ∀ (g : Perm α), g ∈ [] → IsSwap g
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
simp (config := { contextual := true }) only [hl.left.symm, List.prod_nil, forall_true_iff]
case intro.mk.cons
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
⊢ P f
case intro.mk.cons
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
intro h1 hmul_swap
case intro.mk.cons.intro.intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
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
case intro.mk.cons
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
⊢ P f
rcases hl.2 g (by simp) with ⟨x, y, hxy⟩
case intro.mk.cons.intro.intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
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 * List.prod l)
case intro.mk.cons.intro.intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
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
rw [← hl.1, List.prod_cons, hxy.2]
no goals
case intro.mk.cons.intro.intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
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 * List.prod l)
exact
  hmul_swap _ _ _ hxy.1
    (ih _ ⟨rfl, fun v hv => hl.2 _ (List.mem_cons_of_mem _ hv)⟩ h1 hmul_swap)
no goals
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
⊢ g ∈ g :: l
simp