awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
refine_1 : Nat.Partition.parts (n := Fintype.card α) σ.partition = Nat.Partition.parts (n := Fintype.card α) τ.partition
⊢ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
have refine_1₁ : σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 = Nat.Partition.parts (n := Fintype.card α) τ.partition
Tactic: rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType,
      h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
refine_1 : Nat.Partition.parts (n := Fintype.card α) σ.partition = Nat.Partition.parts (n := Fintype.card α) τ.partition
refine_1₁ :
  σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 =
    Nat.Partition.parts (n := Fintype.card α) τ.partition
⊢ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
have refine_1₂ : σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 =
  τ.cycleType + Multiset.replicate (Fintype.card α - #τ.support) 1
Tactic: rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType,
      h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
refine_1 : Nat.Partition.parts (n := Fintype.card α) σ.partition = Nat.Partition.parts (n := Fintype.card α) τ.partition
refine_1₁ :
  σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 =
    Nat.Partition.parts (n := Fintype.card α) τ.partition
refine_1₂ :
  σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 =
    τ.cycleType + Multiset.replicate (Fintype.card α - #τ.support) 1
⊢ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
have refine_1₃ : σ.cycleType + Multiset.replicate (Fintype.card α - σ.cycleType.sum) 1 =
  τ.cycleType + Multiset.replicate (Fintype.card α - #τ.support) 1
Tactic: rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType,
      h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
refine_1 : Nat.Partition.parts (n := Fintype.card α) σ.partition = Nat.Partition.parts (n := Fintype.card α) τ.partition
refine_1₁ :
  σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 =
    Nat.Partition.parts (n := Fintype.card α) τ.partition
refine_1₂ :
  σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 =
    τ.cycleType + Multiset.replicate (Fintype.card α - #τ.support) 1
refine_1₃ :
  σ.cycleType + Multiset.replicate (Fintype.card α - σ.cycleType.sum) 1 =
    τ.cycleType + Multiset.replicate (Fintype.card α - #τ.support) 1
⊢ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
have refine_1₄ : σ.cycleType + Multiset.replicate (Fintype.card α - σ.cycleType.sum) 1 =
  τ.cycleType + Multiset.replicate (Fintype.card α - τ.cycleType.sum) 1
Tactic: rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType,
      h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
refine_1 : Nat.Partition.parts (n := Fintype.card α) σ.partition = Nat.Partition.parts (n := Fintype.card α) τ.partition
refine_1₁ :
  σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 =
    Nat.Partition.parts (n := Fintype.card α) τ.partition
refine_1₂ :
  σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 =
    τ.cycleType + Multiset.replicate (Fintype.card α - #τ.support) 1
refine_1₃ :
  σ.cycleType + Multiset.replicate (Fintype.card α - σ.cycleType.sum) 1 =
    τ.cycleType + Multiset.replicate (Fintype.card α - #τ.support) 1
refine_1₄ :
  σ.cycleType + Multiset.replicate (Fintype.card α - σ.cycleType.sum) 1 =
    τ.cycleType + Multiset.replicate (Fintype.card α - τ.cycleType.sum) 1
⊢ Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
have refine_1₅ : τ.cycleType + Multiset.replicate (Fintype.card α - τ.cycleType.sum) 1 =
  τ.cycleType + Multiset.replicate (Fintype.card α - τ.cycleType.sum) 1
Tactic: rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType,
      h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
⊢ σ.cycleType = τ.cycleType
have refine_2 : Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) σ.partition) = τ.cycleType
Tactic: rw [← filter_parts_partition_eq_cycleType, ← filter_parts_partition_eq_cycleType, h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
refine_2 : Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) σ.partition) = τ.cycleType
⊢ σ.cycleType = τ.cycleType
have refine_2₁ : Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) σ.partition) =
  Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) τ.partition)
Tactic: rw [← filter_parts_partition_eq_cycleType, ← filter_parts_partition_eq_cycleType, h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : Eq (α := (Fintype.card α).Partition) σ.partition τ.partition
refine_2 : Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) σ.partition) = τ.cycleType
refine_2₁ :
  Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) σ.partition) =
    Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) τ.partition)
⊢ σ.cycleType = τ.cycleType
have refine_2₂ : Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) τ.partition) =
  Multiset.filter (fun (n : ℕ) ↦ 2 ≤ n) (Nat.Partition.parts (n := Fintype.card α) τ.partition)
Tactic: rw [← filter_parts_partition_eq_cycleType, ← filter_parts_partition_eq_cycleType, h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ σ.IsSwap ↔ σ.cycleType = {2}
have mp : σ.IsSwap → σ.cycleType = {2}
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
mp : σ.IsSwap → σ.cycleType = {2}
⊢ σ.IsSwap ↔ σ.cycleType = {2}
have mpr : σ.cycleType = {2} → σ.IsSwap
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
σ : Perm α
h : σ.IsSwap
⊢ _root_.orderOf σ = 2
have have : ∀ (this : Fintype α), _root_.orderOf σ = 2
Tactic: have := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
σ : Perm α
h : σ.IsSwap
this : Fintype α
⊢ _root_.orderOf σ = 2
have rw : σ.cycleType.lcm = 2
Tactic: rw [← lcm_cycleType, isSwap_iff_cycleType.mp h, Multiset.lcm_singleton, normalize_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
σ : Perm α
h : σ.IsSwap
this : Fintype α
rw : σ.cycleType.lcm = 2
⊢ _root_.orderOf σ = 2
have rw₁ : Eq (α := ℕ) (Multiset.lcm {2}) 2
Tactic: rw [← lcm_cycleType, isSwap_iff_cycleType.mp h, Multiset.lcm_singleton, normalize_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
σ : Perm α
h : σ.IsSwap
this : Fintype α
rw : σ.cycleType.lcm = 2
rw₁ : Eq (α := ℕ) (Multiset.lcm {2}) 2
⊢ _root_.orderOf σ = 2
have rw₂ : Eq (α := ℕ) ((normalize : (a : ℕ) → ℕ) 2 : ℕ) (2 : ℕ)
Tactic: rw [← lcm_cycleType, isSwap_iff_cycleType.mp h, Multiset.lcm_singleton, normalize_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Finite α
σ : Perm α
h : σ.IsSwap
this : Fintype α
rw : σ.cycleType.lcm = 2
rw₁ : Eq (α := ℕ) (Multiset.lcm {2}) 2
rw₂ : Eq (α := ℕ) ((normalize : (a : ℕ) → ℕ) 2 : ℕ) (2 : ℕ)
⊢ _root_.orderOf σ = 2
have rw₃ : Eq (α := ℕ) 2 2
Tactic: rw [← lcm_cycleType, isSwap_iff_cycleType.mp h, Multiset.lcm_singleton, normalize_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ #σ.support = 3
have rw : σ.cycleType.sum = 3
Tactic: rw [← sum_cycleType, h.cycleType, Multiset.sum_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
rw : σ.cycleType.sum = 3
⊢ #σ.support = 3
have rw₁ : Eq (α := ℕ) (Multiset.sum {3}) 3
Tactic: rw [← sum_cycleType, h.cycleType, Multiset.sum_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
rw : σ.cycleType.sum = 3
rw₁ : Eq (α := ℕ) (Multiset.sum {3}) 3
⊢ #σ.support = 3
have rw₂ : Eq (α := ℕ) 3 3
Tactic: rw [← sum_cycleType, h.cycleType, Multiset.sum_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
⊢ #σ.support = 3 ↔ σ.IsThreeCycle
have refine : ∀ (h : #σ.support = 3), σ.IsThreeCycle
Tactic: refine ⟨fun h => ?_, IsThreeCycle.card_support⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
⊢ σ.IsThreeCycle
have pos : ∀ (h0 : σ.cycleType = 0), σ.IsThreeCycle
Tactic: by_cases h0 : σ.cycleType = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
pos : ∀ (h0 : σ.cycleType = 0), σ.IsThreeCycle
⊢ σ.IsThreeCycle
have neg : ∀ (h0 : ¬σ.cycleType = 0), σ.IsThreeCycle
Tactic: by_cases h0 : σ.cycleType = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : σ.cycleType = 0
⊢ σ.IsThreeCycle
have h₁ : Eq (α := ℕ) 0 3
Tactic: rw [← sum_cycleType, h0, sum_zero] at h
Cleared hypotheses: h, h0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
⊢ σ.IsThreeCycle
have neg : ∀ (n : ℕ) (hn : n ∈ σ.cycleType), σ.IsThreeCycle
Tactic: obtain ⟨n, hn⟩ := exists_mem_of_ne_zero h0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
⊢ σ.IsThreeCycle
have pos : ∀ (h1 : σ.cycleType.erase n = 0), σ.IsThreeCycle
Tactic: by_cases h1 : σ.cycleType.erase n = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
pos : ∀ (h1 : σ.cycleType.erase n = 0), σ.IsThreeCycle
⊢ σ.IsThreeCycle
have neg : ∀ (h1 : ¬σ.cycleType.erase n = 0), σ.IsThreeCycle
Tactic: by_cases h1 : σ.cycleType.erase n = 0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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
⊢ σ.IsThreeCycle
have pos : ∀ (h0 : ¬σ.cycleType = 0) (n : ℕ) (h : n = 3) (hn : n ∈ σ.cycleType) (h1 : σ.cycleType.erase n = 0), σ.IsThreeCycle
Tactic: rw [← sum_cycleType, ← cons_erase hn, h1, cons_zero, Multiset.sum_singleton] at h
Cleared hypotheses: h, h0, n, hn, h1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : n = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
⊢ σ.IsThreeCycle
have pos : σ.cycleType = {3}
Tactic: rw [IsThreeCycle, ← cons_erase hn, h1, h, ← cons_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : n = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
pos : σ.cycleType = {3}
⊢ σ.IsThreeCycle
have pos₁ : n ::ₘ σ.cycleType.erase n = {3}
Tactic: rw [IsThreeCycle, ← cons_erase hn, h1, h, ← cons_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : n = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
pos : σ.cycleType = {3}
pos₁ : n ::ₘ σ.cycleType.erase n = {3}
⊢ σ.IsThreeCycle
have pos₂ : n ::ₘ 0 = {3}
Tactic: rw [IsThreeCycle, ← cons_erase hn, h1, h, ← cons_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : n = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
pos : σ.cycleType = {3}
pos₁ : n ::ₘ σ.cycleType.erase n = {3}
pos₂ : n ::ₘ 0 = {3}
⊢ σ.IsThreeCycle
have pos₃ : Eq (α := Multiset ℕ) (3 ::ₘ 0) {3}
Tactic: rw [IsThreeCycle, ← cons_erase hn, h1, h, ← cons_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : n = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
pos : σ.cycleType = {3}
pos₁ : n ::ₘ σ.cycleType.erase n = {3}
pos₂ : n ::ₘ 0 = {3}
pos₃ : Eq (α := Multiset ℕ) (3 ::ₘ 0) {3}
⊢ σ.IsThreeCycle
have pos₄ : Eq (α := Multiset ℕ) (3 ::ₘ 0) (3 ::ₘ 0)
Tactic: rw [IsThreeCycle, ← cons_erase hn, h1, h, ← cons_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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
⊢ σ.IsThreeCycle
have neg : ∀ (m : ℕ) (hm : m ∈ σ.cycleType.erase n), σ.IsThreeCycle
Tactic: obtain ⟨m, hm⟩ := exists_mem_of_ne_zero h1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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
⊢ σ.IsThreeCycle
have 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
Tactic: rw [← sum_cycleType, ← cons_erase hn, ← cons_erase hm, Multiset.sum_cons, Multiset.sum_cons] at h
Cleared hypotheses: h, h0, n, hn, h1, m, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
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
⊢ σ.IsThreeCycle
have this : ∀ {k : ℕ}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False
Tactic: have : ∀ {k}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False := by lia
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ σ.IsCycle
have rw : σ.cycleType.card = 1
Tactic: rw [← card_cycleType_eq_one, h.cycleType, card_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
rw : σ.cycleType.card = 1
⊢ σ.IsCycle
have rw₁ : card (α := ℕ) {3} = 1
Tactic: rw [← card_cycleType_eq_one, h.cycleType, card_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
rw : σ.cycleType.card = 1
rw₁ : card (α := ℕ) {3} = 1
⊢ σ.IsCycle
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [← card_cycleType_eq_one, h.cycleType, card_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ Eq (α := ℤˣ) (((Perm.sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (1 : ℤˣ)
have rw : HPow.hPow (α := ℤˣ) (-1) (Multiset.sum {3} + card (α := ℕ) {3}) = 1
Tactic: rw [Equiv.Perm.sign_of_cycleType, h.cycleType]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
h : f.IsThreeCycle
⊢ f⁻¹.IsThreeCycle
have rwa : f⁻¹.cycleType = {3}
Tactic: rwa [IsThreeCycle, cycleType_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
h : f.IsThreeCycle
rwa : f⁻¹.cycleType = {3}
⊢ f⁻¹.IsThreeCycle
have rwa₁ : f.cycleType = {3}
Tactic: rwa [IsThreeCycle, cycleType_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
⊢ f⁻¹.IsThreeCycle → f.IsThreeCycle
have rw : f⁻¹⁻¹⁻¹.IsThreeCycle → f⁻¹⁻¹.IsThreeCycle
Tactic: rw [← inv_inv f]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ _root_.orderOf g = 3
have rw : g.cycleType.lcm = 3
Tactic: rw [← lcm_cycleType, ht.cycleType, Multiset.lcm_singleton, normalize_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
rw : g.cycleType.lcm = 3
⊢ _root_.orderOf g = 3
have rw₁ : Eq (α := ℕ) (Multiset.lcm {3}) 3
Tactic: rw [← lcm_cycleType, ht.cycleType, Multiset.lcm_singleton, normalize_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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
⊢ _root_.orderOf g = 3
have rw₂ : Eq (α := ℕ) ((normalize : (a : ℕ) → ℕ) 3 : ℕ) (3 : ℕ)
Tactic: rw [← lcm_cycleType, ht.cycleType, Multiset.lcm_singleton, normalize_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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 : ℕ)
⊢ _root_.orderOf g = 3
have rw₃ : Eq (α := ℕ) 3 3
Tactic: rw [← lcm_cycleType, ht.cycleType, Multiset.lcm_singleton, normalize_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ (g * g).IsThreeCycle
have rw : Nat.Coprime 2 (_root_.orderOf g)
Tactic: rw [← pow_two, ← card_support_eq_three_iff, support_pow_coprime, ht.card_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ Nat.Coprime 2 (_root_.orderOf g)
have rw : Nat.Coprime 2 3
Tactic: rw [ht.orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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}
⊢ (swap a b * swap a c).IsThreeCycle
have rw : Finset.card (α := α) {a, b, c} = 3
Tactic: rw [← card_support_eq_three_iff, h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ (swap a b * swap a c).IsThreeCycle
have suffices : (swap a b * swap a c).support = {a, b, c}
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
⊢ (swap a b * swap a c).support = {a, b, c}
have apply : ∀ x ∈ (swap a b).support ⊔ (swap a c).support, Membership.mem (γ := Finset α) {a, b, c} x
Tactic: apply le_antisymm ((support_mul_le _ _).trans fun x => _) fun x hx => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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
⊢ (swap a b * swap a c).support = {a, b, c}
have apply₁ : ∀ (x : α) (hx : Membership.mem (γ := Finset α) {a, b, c} x), x ∈ (swap a b * swap a c).support
Tactic: apply le_antisymm ((support_mul_le _ _).trans fun x => _) fun x hx => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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
⊢ x ∈ (swap a b * swap a c).support
have simp : Function.comp (β := α) (⇑(swap a b) : (a : α) → α) (⇑(swap a c) : (a : α) → α) x ≠ x
Tactic: simp only [mem_support, coe_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ g.support =
      insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) ↔
    a ∈ g.support
have mp : g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α)
        (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) →
  a ∈ g.support
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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
⊢ g.support =
      insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) ↔
    a ∈ g.support
have mpr : a ∈ g.support →
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
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 : α) : α)))
have mpr : insert a
    (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) =
  g.support
Tactic: symm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ insert a
      (insert (α := α) ((g : (a : α) → α) a : α)
        (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) =
    g.support
have mpr : insert a
    (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) ⊆
  g.support
Tactic: apply Finset.eq_of_subset_of_card_le