internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.existsBasis
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
hsupp_ne : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑c).Nonempty
⊢ Nonempty (Equiv.Perm.Basis g)
Tactic:
exact ⟨fun c ↦ (hsupp_ne c).choose, fun c ↦ (hsupp_ne c).choose_spec⟩
Proof state after:
no goals
Theorem: OnCycleFactors.Kf_mul_add
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i j : ℤ
⊢ Kf a (e' * e) (c, i + j) = (g ^ i) (Kf a e' (e c, j))
Tactic:
simp only [Kf_def, zpow_add, Equiv.Perm.coe_mul, Function.comp_apply]
Proof state after:
no goals
Theorem: OnCycleFactors.Kf_add
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i j : ℤ
⊢ Kf a e (c, i + j) = (g ^ i) (Kf a 1 (e c, j))
Tactic:
rw [← Kf_mul_add, one_mul]
Proof state after:
no goals
Theorem: OnCycleFactors.Kf_add'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i j : ℤ
⊢ Kf a e (c, i + j) = (g ^ i) (Kf a e (c, j))
Tactic:
rw [← mul_one e, Kf_mul_add, mul_one]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i j : ℤ
⊢ (g ^ i) (Kf a e (1 c, j)) = (g ^ i) (Kf a e (c, j))
Theorem: OnCycleFactors.Kf_add'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i j : ℤ
⊢ (g ^ i) (Kf a e (1 c, j)) = (g ^ i) (Kf a e (c, j))
Tactic:
rfl
Proof state after:
no goals
Theorem: Equiv.Perm.Basis.eq_cycleOf
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ ↑c = Equiv.Perm.cycleOf g ((g ^ i) (a c))
Tactic:
rw [Equiv.Perm.cycleOf_self_apply_zpow]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ ↑c = Equiv.Perm.cycleOf g (a c)
Theorem: Equiv.Perm.Basis.eq_cycleOf
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ ↑c = Equiv.Perm.cycleOf g (a c)
Tactic:
rw [a.cycleOf_eq]
Proof state after:
no goals
Theorem: Equiv.Perm.Basis.eq_cycleOf'
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
e : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ ↑(e c) = Equiv.Perm.cycleOf g (Kf a e (c, i))
Tactic:
rw [Kf_def, Equiv.Perm.cycleOf_self_apply_zpow, a.cycleOf_eq]
Proof state after:
no goals
Theorem: Equiv.Perm.Basis.Kf_apply
Proof 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 : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ g (Kf a e (c, i)) = Kf a e (c, i + 1)
Tactic:
rw [Kf_def, Kf_def, ← Equiv.Perm.mul_apply, ← zpow_one_add, add_comm 1 i]
Proof state after:
no goals
Theorem: Equiv.Perm.Basis.Kf_apply'
Proof 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 + 1)
Tactic:
rw [hd]
Proof 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
⊢ ↑(e c) (Kf a e (c, i)) = Kf a e (c, i + 1)
Theorem: Equiv.Perm.Basis.Kf_apply'
Proof 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
⊢ ↑(e c) (Kf a e (c, i)) = Kf a e (c, i + 1)
Tactic:
rw [Equiv.Perm.Basis.eq_cycleOf', Equiv.Perm.cycleOf_apply_self,
  Equiv.Perm.Basis.Kf_apply]
Proof state after:
no goals
Theorem: Equiv.Perm.Basis.Kf_apply''
Proof 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
Proof 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)
Theorem: Equiv.Perm.Basis.Kf_apply''
Proof 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
Proof 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)
Theorem: Equiv.Perm.Basis.Kf_apply''
Proof 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]
Proof 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
Theorem: Equiv.Perm.Basis.Kf_apply''
Proof 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'
Proof state after:
no goals
Theorem: Equiv.Perm.Basis.Kf_apply''
Proof 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⟩))
Proof 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)
Theorem: Equiv.Perm.Basis.Kf_apply''
Proof 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']
Proof 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
Theorem: Equiv.Perm.Basis.Kf_apply''
Proof 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
Proof 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)
Theorem: Equiv.Perm.Basis.Kf_apply''
Proof 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
Proof state after:
no goals
Theorem: Equiv.Perm.Basis.Kf_factorsThrough
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
⊢ Function.FactorsThrough (Kf a e') (Kf a e)
Tactic:
rintro ⟨c, i⟩ ⟨d, j⟩ He
Proof state after:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : Kf a e (c, i) = Kf a e (d, j)
⊢ Kf a e' (c, i) = Kf a e' (d, j)
Theorem: Equiv.Perm.Basis.Kf_factorsThrough
Proof state before:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : Kf a e (c, i) = Kf a e (d, j)
⊢ Kf a e' (c, i) = Kf a e' (d, j)
Tactic:
simp only [Kf_def] at He ⊢
Proof state after:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e c)) = (g ^ j) (a (e d))
⊢ (g ^ i) (a (e' c)) = (g ^ j) (a (e' d))
Theorem: Equiv.Perm.Basis.Kf_factorsThrough
Proof state before:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e c)) = (g ^ j) (a (e d))
⊢ c = d
Tactic:
apply Equiv.injective e
Proof state after:
case mk.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e c)) = (g ^ j) (a (e d))
⊢ e c = e d
Theorem: Equiv.Perm.Basis.Kf_factorsThrough
Proof state before:
case mk.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e c)) = (g ^ j) (a (e d))
⊢ e c = e d
Tactic:
rw [← Subtype.coe_inj, Equiv.Perm.Basis.eq_cycleOf, Equiv.Perm.Basis.eq_cycleOf, He]
Proof state after:
no goals
Theorem: Equiv.Perm.Basis.Kf_factorsThrough
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e c)) = (g ^ j) (a (e d))
hcd : c = d
⊢ (g ^ i) (a (e' c)) = (g ^ j) (a (e' d))
Tactic:
rw [hcd] at He ⊢
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ (g ^ i) (a (e' d)) = (g ^ j) (a (e' d))
Theorem: Equiv.Perm.Basis.Kf_factorsThrough
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ (g ^ i) (a (e' d)) = (g ^ j) (a (e' d))
Tactic:
rw [g.zpow_eq_zpow_on_iff i j,
  ← Equiv.Perm.cycle_is_cycleOf (a := a (e d)) (a.mem_support _) (e d).prop] at He
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ (g ^ i) (a (e' d)) = (g ^ j) (a (e' d))

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ g (a (e d)) ≠ a (e d)
Theorem: Equiv.Perm.Basis.Kf_factorsThrough
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ (g ^ i) (a (e' d)) = (g ^ j) (a (e' d))

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ g (a (e d)) ≠ a (e d)
Tactic:
rw [g.zpow_eq_zpow_on_iff,
  ← Equiv.Perm.cycle_is_cycleOf (a := a (e' d)) (a.mem_support _) (e' d).prop, ← hee' d]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ g (a (e' d)) ≠ a (e' d)

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ g (a (e d)) ≠ a (e d)
Theorem: Equiv.Perm.Basis.Kf_factorsThrough
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ g (a (e' d)) ≠ a (e' d)

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ g (a (e d)) ≠ a (e d)
Tactic:
exact He
Proof state after:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ g (a (e' d)) ≠ a (e' d)

case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : (g ^ i) (a (e d)) = (g ^ j) (a (e d))
hcd : c = d
⊢ g (a (e d)) ≠ a (e d)
Theorem: Equiv.Perm.Basis.Kf_factorsThrough
Proof state before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ g (a (e' d)) ≠ a (e' d)
Tactic:
rw [← Equiv.Perm.mem_support, ← Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff,
  ← Equiv.Perm.cycle_is_cycleOf (a := a (e' d)) (a.mem_support _) (e' d).prop]
Proof state after:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ ↑(e' d) ∈ Equiv.Perm.cycleFactorsFinset g
Theorem: Equiv.Perm.Basis.Kf_factorsThrough
Proof state before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
e e' : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hee' :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }),
    (Equiv.Perm.support ↑(e c)).card = (Equiv.Perm.support ↑(e' c)).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
He : i % ↑(Equiv.Perm.support ↑(e d)).card = j % ↑(Equiv.Perm.support ↑(e d)).card
hcd : c = d
⊢ ↑(e' d) ∈ Equiv.Perm.cycleFactorsFinset g
Tactic:
exact (e' d).prop
Proof state after:
no goals