α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx : ∀ (f : Perm α), f ∈ l → ¬x ∈ support f
⊢ ¬x ∈ support (List.prod l)
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx : x ∈ support (List.prod l)
⊢ ∃ f, f ∈ l ∧ x ∈ support f
contrapose! hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx : ∀ (f : Perm α), f ∈ l → ↑f x = x
⊢ ↑(List.prod l) x = x
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx : ∀ (f : Perm α), f ∈ l → ¬x ∈ support f
⊢ ¬x ∈ support (List.prod l)
simp_rw [mem_support, not_not] at hx⊢
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l → ↑f x = x
hx : ∀ (f : Perm α), f ∈ [] → ↑f x = x
⊢ ↑(List.prod []) x = x

case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ ↑(List.prod (f :: l)) x = x
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx : ∀ (f : Perm α), f ∈ l → ↑f x = x
⊢ ↑(List.prod l) x = x
induction' l with f l ih
no goals
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l → ↑f x = x
hx : ∀ (f : Perm α), f ∈ [] → ↑f x = x
⊢ ↑(List.prod []) x = x
rfl
case cons._
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ f ∈ f :: l

case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ ∀ (f : Perm α), f ∈ l → ↑f x = x
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ ↑(List.prod (f :: l)) x = x
rw [List.prod_cons, mul_apply, ih, hx]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ ∀ (f : Perm α), f ∈ l → ↑f x = x
case cons._
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ f ∈ f :: l

case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ ∀ (f : Perm α), f ∈ l → ↑f x = x
simp only [List.find?, List.mem_cons, true_or]
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
f' : Perm α
hf' : f' ∈ l
⊢ ↑f' x = x
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
⊢ ∀ (f : Perm α), f ∈ l → ↑f x = x
intros f' hf'
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
f' : Perm α
hf' : f' ∈ l
⊢ f' ∈ f :: l
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
f' : Perm α
hf' : f' ∈ l
⊢ ↑f' x = x
refine' hx f' _
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
f' : Perm α
hf' : f' ∈ l
⊢ f' = f ∨ f' ∈ l
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
f' : Perm α
hf' : f' ∈ l
⊢ f' ∈ f :: l
simp only [List.find?, List.mem_cons]
no goals
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
l✝ : List (Perm α)
x : α
hx✝ : ∀ (f : Perm α), f ∈ l✝ → ↑f x = x
f : Perm α
l : List (Perm α)
ih : (∀ (f : Perm α), f ∈ l → ↑f x = x) → ↑(List.prod l) x = x
hx : ∀ (f_1 : Perm α), f_1 ∈ f :: l → ↑f_1 x = x
f' : Perm α
hf' : f' ∈ l
⊢ f' = f ∨ f' ∈ l
exact Or.inr hf'