awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
h1 : ¬σ.cycleType.erase n = 0
neg : ∀ (m : ℕ) (hm : m ∈ σ.cycleType.erase n), σ.IsThreeCycle
⊢ σ.IsThreeCycle

Tactic:
obtain ⟨m, hm⟩ := exists_mem_of_ne_zero h1

Premises used: Multiset.exists_mem_of_ne_zero
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
h1 : ¬σ.cycleType.erase n = 0
m : ℕ
hm : m ∈ σ.cycleType.erase n
neg :
  ∀ (h0 : ¬σ.cycleType = 0) (n : ℕ) (hn : n ∈ σ.cycleType) (h1 : ¬σ.cycleType.erase n = 0) (m : ℕ)
    (h : n + (m + ((σ.cycleType.erase n).erase m).sum) = 3) (hm : m ∈ σ.cycleType.erase n), σ.IsThreeCycle
⊢ σ.IsThreeCycle

Tactic:
rw [← sum_cycleType, ← cons_erase hn, ← cons_erase hm, Multiset.sum_cons, Multiset.sum_cons] at h

Premises used: Multiset.cons_erase, Multiset.sum_cons, Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
h1 : ¬σ.cycleType.erase n = 0
m : ℕ
h : n + (m + ((σ.cycleType.erase n).erase m).sum) = 3
hm : m ∈ σ.cycleType.erase n
⊢ ∀ {k : ℕ}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False

Tactic:
lia
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
h1 : ¬σ.cycleType.erase n = 0
m : ℕ
h : n + (m + ((σ.cycleType.erase n).erase m).sum) = 3
hm : m ∈ σ.cycleType.erase n
⊢ ∀ {k : ℕ}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False

Tactic:
have : ∀ {k}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False := by lia
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
h1 : ¬σ.cycleType.erase n = 0
m : ℕ
h : n + (m + ((σ.cycleType.erase n).erase m).sum) = 3
hm : m ∈ σ.cycleType.erase n
this : ∀ {k : ℕ}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False
⊢ σ.IsThreeCycle

Tactic:
cases this (two_le_of_mem_cycleType (mem_of_mem_erase hm)) (two_le_of_mem_cycleType hn) h

Premises used: Equiv.Perm.two_le_of_mem_cycleType, Multiset.mem_of_mem_erase
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
rw : σ.cycleType.card = 1
rw₁ : card (α := ℕ) {3} = 1
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ σ.IsCycle

Tactic:
rw [← card_cycleType_eq_one, h.cycleType, card_singleton]

Premises used: Equiv.Perm.card_cycleType_eq_one, Multiset.card_singleton, Equiv.Perm.IsThreeCycle.cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
rw : HPow.hPow (α := ℤˣ) (-1) (Multiset.sum {3} + card (α := ℕ) {3}) = 1
⊢ Eq (α := ℤˣ) (((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (1 : ℤˣ)

Tactic:
rw [Equiv.Perm.sign_of_cycleType, h.cycleType]

Premises used: Equiv.Perm.sign_of_cycleType, Equiv.Perm.IsThreeCycle.cycleType
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ HPow.hPow (α := ℤˣ) (-1) (Multiset.sum {3} + card (α := ℕ) {3}) = 1

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
h : f.IsThreeCycle
rwa : f⁻¹.cycleType = {3}
rwa₁ rwa₂ rwa₃ rwa₄ : f.cycleType = {3}
⊢ f⁻¹.IsThreeCycle

Tactic:
rwa [IsThreeCycle, cycleType_inv]

Premises used: Equiv.Perm.cycleType_inv, Equiv.Perm.IsThreeCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
rw : f⁻¹⁻¹⁻¹.IsThreeCycle → f⁻¹⁻¹.IsThreeCycle
⊢ f⁻¹.IsThreeCycle → f.IsThreeCycle

Tactic:
rw [← inv_inv f]

Premises used: inv_inv
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
⊢ f⁻¹⁻¹⁻¹.IsThreeCycle → f⁻¹⁻¹.IsThreeCycle

Tactic:
apply inv

Premises used: Equiv.Perm.IsThreeCycle.inv
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
rw : g.cycleType.lcm = 3
rw₁ : Eq (α := ℕ) (Multiset.lcm {3}) 3
rw₂ : Eq (α := ℕ) ((normalize : (a : ℕ) → ℕ) 3 : ℕ) (3 : ℕ)
rw₃ rw₄ : Eq (α := ℕ) 3 3
⊢ _root_.orderOf g = 3

Tactic:
rw [← lcm_cycleType, ht.cycleType, Multiset.lcm_singleton, normalize_eq]

Premises used: Multiset.lcm_singleton, Equiv.Perm.lcm_cycleType, Equiv.Perm.IsThreeCycle.cycleType, normalize_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
rw : Nat.Coprime 2 (_root_.orderOf g)
⊢ (g * g).IsThreeCycle

Tactic:
rw [← pow_two, ← card_support_eq_three_iff, support_pow_coprime, ht.card_support]

Premises used: pow_two, Equiv.Perm.IsThreeCycle.card_support, card_support_eq_three_iff, Equiv.Perm.support_pow_coprime
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
rw : Nat.Coprime 2 3
⊢ Nat.Coprime 2 (_root_.orderOf g)

Tactic:
rw [ht.orderOf]

Premises used: Equiv.Perm.IsThreeCycle.orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ Nat.Coprime 2 3

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
h : (swap a b * swap a c).support = {a, b, c}
rw : Finset.card (α := α) {a, b, c} = 3
⊢ (swap a b * swap a c).IsThreeCycle

Tactic:
rw [← card_support_eq_three_iff, h]

Premises used: card_support_eq_three_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
h : (swap a b * swap a c).support = {a, b, c}
⊢ Finset.card (α := α) {a, b, c} = 3

Tactic:
simp [ab, ac, bc]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
suffices : (swap a b * swap a c).support = {a, b, c}
⊢ (swap a b * swap a c).IsThreeCycle

Tactic:
suffices h : support (swap a b * swap a c) = {a, b, c} by
    rw [← card_support_eq_three_iff, h]
    simp [ab, ac, bc]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
apply : ∀ x ∈ (swap a b).support ⊔ (swap a c).support, Membership.mem (γ := Finset α) {a, b, c} x
apply₁ : ∀ (x : α) (hx : Membership.mem (γ := Finset α) {a, b, c} x), x ∈ (swap a b * swap a c).support
⊢ (swap a b * swap a c).support = {a, b, c}

Tactic:
apply le_antisymm ((support_mul_le _ _).trans fun x => _) fun x hx => ?_

Premises used: Equiv.Perm.support_mul_le, le_antisymm, LE.le.trans
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ ∀ x ∈ (swap a b).support ⊔ (swap a c).support, Membership.mem (γ := Finset α) {a, b, c} x

Tactic:
simp [ab, ac]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : Membership.mem (γ := Finset α) {a, b, c} x
simp : Function.comp (β := α) (⇑(swap a b) : (a : α) → α) (⇑(swap a c) : (a : α) → α) x ≠ x
⊢ x ∈ (swap a b * swap a c).support

Tactic:
simp only [mem_support, coe_mul]

Premises used: Equiv.Perm.coe_mul, Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : Membership.mem (γ := Finset α) {a, b, c} x
⊢ Function.comp (β := α) (⇑(swap a b) : (a : α) → α) (⇑(swap a c) : (a : α) → α) x ≠ x

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
mp :
  g.support =
      insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) →
    a ∈ g.support
mpr :
  a ∈ g.support →
    g.support =
      insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
⊢ g.support =
      insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) ↔
    a ∈ g.support

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
hg :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
⊢ a ∈ g.support

Tactic:
simp [hg]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
mpr :
  insert a
      (insert (α := α) ((g : (a : α) → α) a : α)
        (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) =
    g.support
⊢ g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))

Tactic:
symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
mpr :
  insert a
      (insert (α := α) ((g : (a : α) → α) a : α)
        (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) ⊆
    g.support
mpr₁ :
  #g.support ≤
    Finset.card (α := α)
      (insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))))
⊢ insert a
      (insert (α := α) ((g : (a : α) → α) a : α)
        (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) =
    g.support

Tactic:
apply Finset.eq_of_subset_of_card_le

Premises used: Finset.eq_of_subset_of_card_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
mpr :
  insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)) ⊆
    g.support
⊢ insert a
      (insert (α := α) ((g : (a : α) → α) a : α)
        (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) ⊆
    g.support

Tactic:
apply Finset.insert_subset ha

Premises used: Finset.insert_subset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
mpr : Membership.mem (α := α) g.support ((g : (a : α) → α) a : α)
mpr₁ : singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) ⊆ g.support
⊢ insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)) ⊆
    g.support

Tactic:
apply Finset.insert_subset

Premises used: Finset.insert_subset
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha mpr mpr₁ mpr₂ mpr₃ : a ∈ g.support
⊢ Membership.mem (α := α) g.support ((g : (a : α) → α) a : α)

Tactic:
rwa [Perm.apply_mem_support]

Premises used: Equiv.Perm.apply_mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) ⊆ g.support

Tactic:
simpa only [Finset.singleton_subset_iff, Perm.apply_mem_support]

Premises used: Finset.singleton_subset_iff, Equiv.Perm.apply_mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
mpr :
  3 ≤
    Finset.card (α := α)
      (insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))))
⊢ #g.support ≤
    Finset.card (α := α)
      (insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))))

Tactic:
rw [hg3.card_support]

Premises used: Equiv.Perm.IsThreeCycle.card_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ ¬(g : (a : α) → α) a = a

Tactic:
simp only [mem_support, ne_eq] at ha

Premises used: Equiv.Perm.mem_support, ne_eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬(g : (a : α) → α) a = a
mpr :
  3 ≤
    Finset.card (α := α)
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) +
      1
mpr₁ :
  a ∉ insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))
⊢ 3 ≤
    Finset.card (α := α)
      (insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))))

Tactic:
rw [Finset.card_insert_eq_ite, if_neg]

Premises used: Finset.card_insert_eq_ite, if_neg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬(g : (a : α) → α) a = a
mpr : 3 ≤ Finset.card (α := α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)) + 1 + 1
mpr₁ : ((g : (a : α) → α) a : α) ∉ singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)
⊢ 3 ≤
    Finset.card (α := α)
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) +
      1

Tactic:
rw [Finset.card_insert_eq_ite, if_neg]

Premises used: Finset.card_insert_eq_ite, if_neg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬(g : (a : α) → α) a = a
⊢ 3 ≤ Finset.card (α := α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)) + 1 + 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬(g : (a : α) → α) a = a
⊢ ((g : (a : α) → α) a : α) ∉ singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)

Tactic:
simpa using Ne.symm ha

Premises used: Ne.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬(g : (a : α) → α) a = a
mpr : ¬(a = (g : (a : α) → α) a ∨ a = (g : (a : α) → α) ((g : (a : α) → α) a : α))
⊢ a ∉ insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton]

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬(g : (a : α) → α) a = a
mpr : ∀ (ha : a = (g : (a : α) → α) a ∨ a = (g : (a : α) → α) ((g : (a : α) → α) a : α)), (g : (a : α) → α) a = a
⊢ ¬(a = (g : (a : α) → α) a ∨ a = (g : (a : α) → α) ((g : (a : α) → α) a : α))

Tactic:
contrapose ha
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a = (g : (a : α) → α) a ∨ a = (g : (a : α) → α) ((g : (a : α) → α) a : α)
mpr : ∀ (ha : a = (g : (a : α) → α) a), (g : (a : α) → α) a = a
mpr₁ : ∀ (ha : a = (g : (a : α) → α) ((g : (a : α) → α) a : α)), (g : (a : α) → α) a = a
⊢ (g : (a : α) → α) a = a

Tactic:
rcases ha with ha | ha
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a = (g : (a : α) → α) a
⊢ (g : (a : α) → α) a = a

Tactic:
ha.symm

Premises used: Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a = (g : (a : α) → α) a
⊢ (g : (a : α) → α) a = a

Tactic:
exact ha.symm

Premises used: Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a = (g : (a : α) → α) ((g : (a : α) → α) a : α)
this : (HPow.hPow (β := ℕ) g 3 : (a : α) → α) a = a
⊢ (g : (a : α) → α) a = a

Tactic:
simpa [pow_succ, ← ha] using this

Premises used: pow_succ
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a = (g : (a : α) → α) ((g : (a : α) → α) a : α)
mpr : (HPow.hPow (β := ℕ) g 3 : (a : α) → α) a = a
⊢ (g : (a : α) → α) a = a

Tactic:
suffices (g ^ 3) a = a by simpa [pow_succ, ← ha] using this
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a = (g : (a : α) → α) ((g : (a : α) → α) a : α)
⊢ (HPow.hPow (β := ℕ) g 3 : (a : α) → α) a = a

Tactic:
simp [← hg3.orderOf]

Premises used: Equiv.Perm.IsThreeCycle.orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
mp : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup → a ∈ g.support
mpr : a ∈ g.support → [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
⊢ [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup ↔ a ∈ g.support

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
mp : (g : (a : α) → α) a ≠ a
⊢ a ∈ g.support

Tactic:
rw [mem_support]

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
⊢ (g : (a : α) → α) a ≠ a

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
mpr :
  g.support =
      insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) →
    [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
⊢ a ∈ g.support → [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup

Tactic:
rw [← support_eq_iff_mem_support hg3]

Premises used: Equiv.Perm.IsThreeCycle.support_eq_iff_mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
this : #g.support = 3
⊢ [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
mpr : #g.support = 3
⊢ [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup

Tactic:
suffices g.support.card = 3 by grind
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
⊢ #g.support = 3

Tactic:
hg3.card_support

Premises used: Equiv.Perm.IsThreeCycle.card_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
⊢ #g.support = 3

Tactic:
exact hg3.card_support

Premises used: Equiv.Perm.IsThreeCycle.card_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
mp :
  g =
      HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) →
    a ∈ g.support
mpr :
  a ∈ g.support →
    g =
      HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
⊢ g =
      HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) ↔
    a ∈ g.support

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
hg :
  g =
    HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
mp : (g : (a : α) → α) a ≠ a
⊢ a ∈ g.support

Tactic:
rw [mem_support]

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
hg :
  g =
    HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
hx : (g : (a : α) → α) a = a
mp : g = 1
⊢ False

Tactic:
apply hg3.isCycle.ne_one

Premises used: Equiv.Perm.IsCycle.ne_one, Equiv.Perm.IsThreeCycle.isCycle
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
hg :
  g =
    HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
hx : (g : (a : α) → α) a = a
⊢ g = 1

Tactic:
simpa [hx] using hg
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))

Tactic:
have ha' := hg3.support_eq_iff_mem_support.mpr ha
-- Module: Mathlib.GroupTheory.Perm.Cycle.Type
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
⊢ [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup

Tactic:
have ha'' := hg3.nodup_iff_mem_support.mpr ha