Theorem: Equiv.Perm.Basis.Kf_apply'' (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
⊢ ↑d (Kf a e (c, i)) = Kf a e (c, i)
Tactic:
suffices hdc : (d : Equiv.Perm α).Disjoint (e c : Equiv.Perm α) by
  apply Or.resolve_right (Equiv.Perm.disjoint_iff_eq_or_eq.mp hdc (Kf a e ⟨c, i⟩))
  rw [Equiv.Perm.Basis.eq_cycleOf', Equiv.Perm.cycleOf_apply_self,
    ← Equiv.Perm.cycleOf_eq_one_iff, ← Equiv.Perm.Basis.eq_cycleOf']
  apply Equiv.Perm.IsCycle.ne_one
  exact (Equiv.Perm.mem_cycleFactorsFinset_iff.mp (e c).prop).1
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
⊢ Equiv.Perm.Disjoint ↑d ↑(e c)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
⊢ Equiv.Perm.Disjoint ↑d ↑(e c)
Tactic:
apply g.cycleFactorsFinset_pairwise_disjoint d.prop (e c).prop
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
⊢ ↑d ≠ ↑(e c)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
⊢ ↑d ≠ ↑(e c)
Tactic:
rw [Function.Injective.ne_iff Subtype.coe_injective]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
⊢ d ≠ e c

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
⊢ d ≠ e c
Tactic:
exact hd'
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
hdc : Equiv.Perm.Disjoint ↑d ↑(e c)
⊢ ↑d (Kf a e (c, i)) = Kf a e (c, i)
Tactic:
apply Or.resolve_right (Equiv.Perm.disjoint_iff_eq_or_eq.mp hdc (Kf a e ⟨c, i⟩))
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
hdc : Equiv.Perm.Disjoint ↑d ↑(e c)
⊢ ¬↑(e c) (Kf a e (c, i)) = Kf a e (c, i)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
hdc : Equiv.Perm.Disjoint ↑d ↑(e c)
⊢ ¬↑(e c) (Kf a e (c, i)) = Kf a e (c, i)
Tactic:
rw [Equiv.Perm.Basis.eq_cycleOf', Equiv.Perm.cycleOf_apply_self,
  ← Equiv.Perm.cycleOf_eq_one_iff, ← Equiv.Perm.Basis.eq_cycleOf']
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
hdc : Equiv.Perm.Disjoint ↑d ↑(e c)
⊢ ¬↑(e c) = 1

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
hdc : Equiv.Perm.Disjoint ↑d ↑(e c)
⊢ ¬↑(e c) = 1
Tactic:
apply Equiv.Perm.IsCycle.ne_one
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
hdc : Equiv.Perm.Disjoint ↑d ↑(e c)
⊢ Equiv.Perm.IsCycle ↑(e c)

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
hd' : d ≠ e c
hdc : Equiv.Perm.Disjoint ↑d ↑(e c)
⊢ Equiv.Perm.IsCycle ↑(e c)
Tactic:
exact (Equiv.Perm.mem_cycleFactorsFinset_iff.mp (e c).prop).1
State after:
no goals