α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑(σ * τ) a = a
⊢ ↑σ a = a ∧ ↑τ a = a
α : Type u_1
f g h σ τ : Perm α
hστ : Disjoint σ τ
a : α
⊢ ↑(σ * τ) a = a ↔ ↑σ a = a ∧ ↑τ a = a
refine' ⟨fun h => _, fun h => by rw [mul_apply, h.2, h.1]⟩
case inl
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑(σ * τ) a = a
hσ : ↑σ a = a
⊢ ↑σ a = a ∧ ↑τ a = a

case inr
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑(σ * τ) a = a
hτ : ↑τ a = a
⊢ ↑σ a = a ∧ ↑τ a = a
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑(σ * τ) a = a
⊢ ↑σ a = a ∧ ↑τ a = a
cases' hστ a with hσ hτ
no goals
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑σ a = a ∧ ↑τ a = a
⊢ ↑(σ * τ) a = a
rw [mul_apply, h.2, h.1]
no goals
case inl
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑(σ * τ) a = a
hσ : ↑σ a = a
⊢ ↑σ a = a ∧ ↑τ a = a
exact ⟨hσ, σ.injective (h.trans hσ.symm)⟩
no goals
case inr
α : Type u_1
f g h✝ σ τ : Perm α
hστ : Disjoint σ τ
a : α
h : ↑(σ * τ) a = a
hτ : ↑τ a = a
⊢ ↑σ a = a ∧ ↑τ a = a
exact ⟨(congr_arg σ hτ).symm.trans h, hτ⟩