-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem Disjoint.disjoint_cycleFactorsFinset {f g : Perm α} (h : Disjoint f g) :
    _root_.Disjoint (cycleFactorsFinset f) (cycleFactorsFinset g)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hf : ∀ (a : α), x a ≠ a → x a = f a
a : α
ha : x a ≠ a
hg : ∀ (a : α), x a ≠ a → x a = g a
⊢ a ∈ f.support ∩ g.support

Tactic:
simp [ha, ← hf a ha, ← hg a ha]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hx : x.IsCycle ∧ ∀ (a : α), x a ≠ a → x a = f a
hy : x.IsCycle ∧ ∀ (a : α), x a ≠ a → x a = g a
⊢ False

Tactic:
obtain ⟨⟨⟨a, ha, -⟩, hf⟩, -, hg⟩ := hx, hy

Result:
case intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hf : ∀ (a : α), x a ≠ a → x a = f a
a : α
ha : x a ≠ a
hg : ∀ (a : α), x a ≠ a → x a = g a
⊢ False

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
⊢ _root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset

Tactic:
rw [Finset.disjoint_left]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
⊢ ∀ ⦃a : Perm α⦄, a ∈ f.cycleFactorsFinset → a ∉ g.cycleFactorsFinset

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
⊢ ∀ ⦃a : Perm α⦄, a ∈ f.cycleFactorsFinset → a ∉ g.cycleFactorsFinset

Tactic:
intro x hx hy

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hx : x ∈ f.cycleFactorsFinset
hy : x ∈ g.cycleFactorsFinset
⊢ False

Proof state:
case intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hf : ∀ (a : α), x a ≠ a → x a = f a
a : α
ha : x a ≠ a
hg : ∀ (a : α), x a ≠ a → x a = g a
⊢ False

Tactic:
have := h.le_bot (by simp [ha, ← hf a ha, ← hg a ha] : a ∈ f.support ∩ g.support)

Result:
case intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hf : ∀ (a : α), x a ≠ a → x a = f a
a : α
ha : x a ≠ a
hg : ∀ (a : α), x a ≠ a → x a = g a
this : a ∈ ⊥
⊢ False

Proof state:
case intro.intro.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hf : ∀ (a : α), x a ≠ a → x a = f a
a : α
ha : x a ≠ a
hg : ∀ (a : α), x a ≠ a → x a = g a
this : a ∈ ⊥
⊢ False

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset

Tactic:
rw [disjoint_iff_disjoint_support] at h

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
⊢ _root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hx : x ∈ f.cycleFactorsFinset
hy : x ∈ g.cycleFactorsFinset
⊢ False

Tactic:
simp only [mem_cycleFactorsFinset_iff, mem_support] at hx hy

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hx : x.IsCycle ∧ ∀ (a : α), x a ≠ a → x a = f a
hy : x.IsCycle ∧ ∀ (a : α), x a ≠ a → x a = g a
⊢ False