ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
⊢ _root_.Disjoint (cycleFactorsFinset f) (cycleFactorsFinset g)
ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : Disjoint f g
⊢ _root_.Disjoint (cycleFactorsFinset f) (cycleFactorsFinset g)
rw [disjoint_iff_disjoint_support] at h
ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
⊢ ∀ ⦃a : Perm α⦄, a ∈ cycleFactorsFinset f → ¬a ∈ cycleFactorsFinset g
ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
⊢ _root_.Disjoint (cycleFactorsFinset f) (cycleFactorsFinset g)
rw [Finset.disjoint_left]
ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
x : Perm α
hx : x ∈ cycleFactorsFinset f
hy : x ∈ cycleFactorsFinset g
⊢ False
ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
⊢ ∀ ⦃a : Perm α⦄, a ∈ cycleFactorsFinset f → ¬a ∈ cycleFactorsFinset g
intro x hx hy
ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
x : Perm α
hx : IsCycle x ∧ ∀ (a : α), ↑x a ≠ a → ↑x a = ↑f a
hy : IsCycle x ∧ ∀ (a : α), ↑x a ≠ a → ↑x a = ↑g a
⊢ False
ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
x : Perm α
hx : x ∈ cycleFactorsFinset f
hy : x ∈ cycleFactorsFinset g
⊢ False
simp only [mem_cycleFactorsFinset_iff, mem_support] at hx hy
case intro.intro.intro.intro
ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
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
ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
x : Perm α
hx : IsCycle x ∧ ∀ (a : α), ↑x a ≠ a → ↑x a = ↑f a
hy : IsCycle x ∧ ∀ (a : α), ↑x a ≠ a → ↑x a = ↑g a
⊢ False
obtain ⟨⟨⟨a, ha, -⟩, hf⟩, -, hg⟩ := hx, hy
case intro.intro.intro.intro
ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
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
case intro.intro.intro.intro
ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
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
have := h.le_bot (by simp [ha, ← hf a ha, ← hg a ha] : a ∈ f.support ∩ g.support)
no goals
case intro.intro.intro.intro
ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
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
tauto
no goals
ι : Type ?u.2757665
α : Type u_1
β : Type ?u.2757671
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h✝ : Disjoint f g
h : _root_.Disjoint (support f) (support g)
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 ∈ support f ∩ support g
simp [ha, ← hf a ha, ← hg a ha]