case nil
α : Type u_1
f g h✝¹ : Perm α
l : List (Perm α)
h✝ : ∀ (g : Perm α), g ∈ l → Disjoint f g
h : ∀ (g : Perm α), g ∈ [] → Disjoint f g
⊢ Disjoint f (List.prod [])

case cons
α : Type u_1
f g✝ h✝¹ : Perm α
l✝ : List (Perm α)
h✝ : ∀ (g : Perm α), g ∈ l✝ → Disjoint f g
g : Perm α
l : List (Perm α)
ih : (∀ (g : Perm α), g ∈ l → Disjoint f g) → Disjoint f (List.prod l)
h : ∀ (g_1 : Perm α), g_1 ∈ g :: l → Disjoint f g_1
⊢ Disjoint f (List.prod (g :: l))
α : Type u_1
f g h✝ : Perm α
l : List (Perm α)
h : ∀ (g : Perm α), g ∈ l → Disjoint f g
⊢ Disjoint f (List.prod l)
induction' l with g l ih
no goals
case nil
α : Type u_1
f g h✝¹ : Perm α
l : List (Perm α)
h✝ : ∀ (g : Perm α), g ∈ l → Disjoint f g
h : ∀ (g : Perm α), g ∈ [] → Disjoint f g
⊢ Disjoint f (List.prod [])
exact disjoint_one_right _
case cons
α : Type u_1
f g✝ h✝¹ : Perm α
l✝ : List (Perm α)
h✝ : ∀ (g : Perm α), g ∈ l✝ → Disjoint f g
g : Perm α
l : List (Perm α)
ih : (∀ (g : Perm α), g ∈ l → Disjoint f g) → Disjoint f (List.prod l)
h : ∀ (g_1 : Perm α), g_1 ∈ g :: l → Disjoint f g_1
⊢ Disjoint f (g * List.prod l)
case cons
α : Type u_1
f g✝ h✝¹ : Perm α
l✝ : List (Perm α)
h✝ : ∀ (g : Perm α), g ∈ l✝ → Disjoint f g
g : Perm α
l : List (Perm α)
ih : (∀ (g : Perm α), g ∈ l → Disjoint f g) → Disjoint f (List.prod l)
h : ∀ (g_1 : Perm α), g_1 ∈ g :: l → Disjoint f g_1
⊢ Disjoint f (List.prod (g :: l))
rw [List.prod_cons]
no goals
case cons
α : Type u_1
f g✝ h✝¹ : Perm α
l✝ : List (Perm α)
h✝ : ∀ (g : Perm α), g ∈ l✝ → Disjoint f g
g : Perm α
l : List (Perm α)
ih : (∀ (g : Perm α), g ∈ l → Disjoint f g) → Disjoint f (List.prod l)
h : ∀ (g_1 : Perm α), g_1 ∈ g :: l → Disjoint f g_1
⊢ Disjoint f (g * List.prod l)
exact (h _ (List.mem_cons_self _ _)).mul_right (ih fun g hg => h g (List.mem_cons_of_mem _ hg))