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 α
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
⊢ insert a
      (insert (α := α) ((g : (a : α) → α) a : α)
        (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) =
    g.support
have mpr₁ : #g.support ≤
  Finset.card (α := α)
    (insert a
      (insert (α := α) ((g : (a : α) → α) a : α)
        (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))))
Tactic: apply Finset.eq_of_subset_of_card_le
-- 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 (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)) ⊆
  g.support
Tactic: apply Finset.insert_subset ha
-- 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 (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)) ⊆
    g.support
have mpr : Membership.mem (α := α) g.support ((g : (a : α) → α) a : α)
Tactic: apply Finset.insert_subset
-- 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
mpr : Membership.mem (α := α) g.support ((g : (a : α) → α) a : α)
⊢ insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)) ⊆
    g.support
have mpr₁ : singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) ⊆ g.support
Tactic: apply Finset.insert_subset
-- 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 ≤
    Finset.card (α := α)
      (insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))))
have mpr : 3 ≤
  Finset.card (α := α)
    (insert a
      (insert (α := α) ((g : (a : α) → α) a : α)
        (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))))
Tactic: rw [hg3.card_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ 3 ≤
    Finset.card (α := α)
      (insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))))
have ha₁ : ¬(g : (a : α) → α) a = a
Tactic: simp only [mem_support, ne_eq] at ha
Cleared hypotheses: ha
-- 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 : ¬(g : (a : α) → α) a = a
⊢ 3 ≤
    Finset.card (α := α)
      (insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))))
have mpr : 3 ≤
  Finset.card (α := α)
      (insert (α := α) ((g : (a : α) → α) a : α)
        (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) +
    1
Tactic: rw [Finset.card_insert_eq_ite, if_neg]
-- 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 : ¬(g : (a : α) → α) a = a
mpr :
  3 ≤
    Finset.card (α := α)
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) +
      1
⊢ 3 ≤
    Finset.card (α := α)
      (insert a
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))))
have mpr₁ : a ∉ insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))
Tactic: rw [Finset.card_insert_eq_ite, if_neg]
-- 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 : ¬(g : (a : α) → α) a = a
⊢ 3 ≤
    Finset.card (α := α)
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) +
      1
have mpr : 3 ≤ Finset.card (α := α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)) + 1 + 1
Tactic: rw [Finset.card_insert_eq_ite, if_neg]
-- 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 : ¬(g : (a : α) → α) a = a
mpr : 3 ≤ Finset.card (α := α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)) + 1 + 1
⊢ 3 ≤
    Finset.card (α := α)
        (insert (α := α) ((g : (a : α) → α) a : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))) +
      1
have mpr₁ : ((g : (a : α) → α) a : α) ∉ singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)
Tactic: rw [Finset.card_insert_eq_ite, if_neg]
-- 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 : ¬(g : (a : α) → α) a = a
⊢ a ∉ insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α))
have mpr : ¬(a = (g : (a : α) → α) a ∨ a = (g : (a : α) → α) ((g : (a : α) → α) a : α))
Tactic: simp only [Finset.mem_insert, Finset.mem_singleton]
-- 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 : ¬(g : (a : α) → α) a = a
⊢ ¬(a = (g : (a : α) → α) a ∨ a = (g : (a : α) → α) ((g : (a : α) → α) a : α))
have mpr : ∀ (ha : a = (g : (a : α) → α) a ∨ a = (g : (a : α) → α) ((g : (a : α) → α) a : α)), (g : (a : α) → α) a = a
Tactic: contrapose ha
Cleared hypotheses: ha
-- 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 : (a : α) → α) a ∨ a = (g : (a : α) → α) ((g : (a : α) → α) a : α)
⊢ (g : (a : α) → α) a = a
have mpr : ∀ (ha : a = (g : (a : α) → α) a), (g : (a : α) → α) a = a
Tactic: rcases ha with ha | ha
Cleared hypotheses: ha
-- 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 : (a : α) → α) a ∨ a = (g : (a : α) → α) ((g : (a : α) → α) a : α)
mpr : ∀ (ha : a = (g : (a : α) → α) a), (g : (a : α) → α) a = a
⊢ (g : (a : α) → α) a = a
have mpr₁ : ∀ (ha : a = (g : (a : α) → α) ((g : (a : α) → α) a : α)), (g : (a : α) → α) a = a
Tactic: rcases ha with ha | ha
Cleared hypotheses: ha
-- 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 : (a : α) → α) ((g : (a : α) → α) a : α)
⊢ (g : (a : α) → α) a = a
have mpr : (HPow.hPow (β := ℕ) g 3 : (a : α) → α) a = a
Tactic: suffices (g ^ 3) a = a by simpa [pow_succ, ← ha] using this
-- 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
⊢ [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup ↔ a ∈ g.support
have mp : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup → 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 : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup → a ∈ g.support
⊢ [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup ↔ a ∈ g.support
have mpr : a ∈ g.support → [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
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 : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
⊢ a ∈ g.support
have mp : (g : (a : α) → α) a ≠ a
Tactic: rw [mem_support]
-- 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
⊢ a ∈ g.support → [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
have 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
Tactic: rw [← support_eq_iff_mem_support hg3]
-- 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 :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
⊢ [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
have mpr : #g.support = 3
Tactic: suffices g.support.card = 3 by grind
-- 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 =
      HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) ↔
    a ∈ g.support
have mp : g =
    HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) →
  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 =
      HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) →
    a ∈ g.support
⊢ g =
      HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
        (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) ↔
    a ∈ g.support
have mpr : a ∈ g.support →
  g =
    HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
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
hg :
  g =
    HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
⊢ a ∈ g.support
have mp : (g : (a : α) → α) a ≠ a
Tactic: rw [mem_support]
-- 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
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
⊢ False
have mp : g = 1
Tactic: apply hg3.isCycle.ne_one
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ g =
    HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
have ha' : 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
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
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 : α) : α)))
⊢ g =
    HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
have ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
Tactic: have ha'' := hg3.nodup_iff_mem_support.mpr ha
-- 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
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
⊢ g =
    HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
      (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α)
have mpr : ∀ (x : α),
  Eq (α := α) ((g : (a : α) → α) x : α)
    ((HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
            (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) :
          (a : α) → α)
        x :
      α)
Tactic: ext x
-- 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
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((HMul.hMul (β := Perm α) (swap a ((g : (a : α) → α) a))
            (swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) :
          (a : α) → α)
        x :
      α)
have mpr : Eq (α := α) ((g : (a : α) → α) x : α)
  ((swap a ((g : (a : α) → α) a) : (a : α) → α)
      (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
    α)
Tactic: simp only [coe_mul, Function.comp_apply]
-- 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
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
      α)
have pos : ∀ (h : x ∈ g.support),
  Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
      α)
Tactic: by_cases h : x ∈ g.support
-- 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
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
pos :
  ∀ (h : x ∈ g.support),
    Eq (α := α) ((g : (a : α) → α) x : α)
      ((swap a ((g : (a : α) → α) a) : (a : α) → α)
          (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
        α)
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
      α)
have neg : ∀ (h : x ∉ g.support),
  Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
      α)
Tactic: by_cases h : x ∈ g.support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (hypothesis)
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 : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x ∈ g.support
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
      α)
have h₁ : x = a ∨ x = (g : (a : α) → α) a ∨ x = (g : (a : α) → α) ((g : (a : α) → α) a : α)
Tactic: simp only [ha', Finset.mem_insert, Finset.mem_singleton] at h
Cleared hypotheses: h
-- 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
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x = a ∨ x = (g : (a : α) → α) a ∨ x = (g : (a : α) → α) ((g : (a : α) → α) a : α)
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
      α)
have pos : ∀ (ha : x ∈ g.support)
  (ha' :
    g.support =
      insert x
        (insert (α := α) ((g : (a : α) → α) x : α)
          (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) x : α) : α))))
  (ha'' : [x, (g : (a : α) → α) x, (g : (a : α) → α) ((g : (a : α) → α) x : α)].Nodup),
  Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap x ((g : (a : α) → α) x) : (a : α) → α)
        (((swap ((g : (a : α) → α) x) ((g : (a : α) → α) ((g : (a : α) → α) x : α)) : Perm α) : (a : α) → α) x : α) :
      α)
Tactic: rcases h with rfl | (rfl | rfl)
Cleared hypotheses: a, ha, ha', ha'', h
-- 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
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x = a ∨ x = (g : (a : α) → α) a ∨ x = (g : (a : α) → α) ((g : (a : α) → α) a : α)
pos :
  ∀ (ha : x ∈ g.support)
    (ha' :
      g.support =
        insert x
          (insert (α := α) ((g : (a : α) → α) x : α)
            (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) x : α) : α))))
    (ha'' : [x, (g : (a : α) → α) x, (g : (a : α) → α) ((g : (a : α) → α) x : α)].Nodup),
    Eq (α := α) ((g : (a : α) → α) x : α)
      ((swap x ((g : (a : α) → α) x) : (a : α) → α)
          (((swap ((g : (a : α) → α) x) ((g : (a : α) → α) ((g : (a : α) → α) x : α)) : Perm α) : (a : α) → α) x : α) :
        α)
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
      α)
have pos₁ : Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)
  ((swap a ((g : (a : α) → α) a) : (a : α) → α)
      (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α)
          ((g : (a : α) → α) a : α) :
        α) :
    α)
Tactic: rcases h with rfl | (rfl | rfl)
Cleared hypotheses: x, h
-- 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
ha' :
  g.support =
    insert a
      (insert (α := α) ((g : (a : α) → α) a : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)))
ha'' : [a, (g : (a : α) → α) a, (g : (a : α) → α) ((g : (a : α) → α) a : α)].Nodup
x : α
h : x = a ∨ x = (g : (a : α) → α) a ∨ x = (g : (a : α) → α) ((g : (a : α) → α) a : α)
pos :
  ∀ (ha : x ∈ g.support)
    (ha' :
      g.support =
        insert x
          (insert (α := α) ((g : (a : α) → α) x : α)
            (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) x : α) : α))))
    (ha'' : [x, (g : (a : α) → α) x, (g : (a : α) → α) ((g : (a : α) → α) x : α)].Nodup),
    Eq (α := α) ((g : (a : α) → α) x : α)
      ((swap x ((g : (a : α) → α) x) : (a : α) → α)
          (((swap ((g : (a : α) → α) x) ((g : (a : α) → α) ((g : (a : α) → α) x : α)) : Perm α) : (a : α) → α) x : α) :
        α)
pos₁ :
  Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α)
            ((g : (a : α) → α) a : α) :
          α) :
      α)
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap a ((g : (a : α) → α) a) : (a : α) → α)
        (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α) x : α) :
      α)
have pos₂ : Eq (α := α) ((g : (a : α) → α) ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) : α)
  ((swap a ((g : (a : α) → α) a) : (a : α) → α)
      (((swap ((g : (a : α) → α) a) ((g : (a : α) → α) ((g : (a : α) → α) a : α)) : Perm α) : (a : α) → α)
          ((g : (a : α) → α) ((g : (a : α) → α) a : α) : α) :
        α) :
    α)
Tactic: rcases h with rfl | (rfl | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Type (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg3 : g.IsThreeCycle
x : α
ha : x ∈ g.support
ha' :
  g.support =
    insert x
      (insert (α := α) ((g : (a : α) → α) x : α) (singleton (α := α) ((g : (a : α) → α) ((g : (a : α) → α) x : α) : α)))
ha'' : [x, (g : (a : α) → α) x, (g : (a : α) → α) ((g : (a : α) → α) x : α)].Nodup
⊢ Eq (α := α) ((g : (a : α) → α) x : α)
    ((swap x ((g : (a : α) → α) x) : (a : α) → α)
        (((swap ((g : (a : α) → α) x) ((g : (a : α) → α) ((g : (a : α) → α) x : α)) : Perm α) : (a : α) → α) x : α) :
      α)
have pos : Eq (α := α) ((g : (a : α) → α) x : α) ((swap x ((g : (a : α) → α) x) : (a : α) → α) x : α)
Tactic: rw [swap_apply_of_ne_of_ne (x := x) (by grind) (by grind)]