awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ : Perm α
h_1 : σ = τ ∨ σ = swap i j * τ
h : σ = swap i j * τ
⊢ τ = swap i j * σ
have rw : τ = swap i j * (swap i j * τ)
Tactic: rw [h, swap_mul_self_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ : Perm α
h_1 : σ = τ ∨ σ = swap i j * τ
h : σ = swap i j * τ
rw : τ = swap i j * (swap i j * τ)
⊢ τ = swap i j * σ
have rw₁ : τ = τ
Tactic: rw [h, swap_mul_self_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ ∨ σ = swap i j * τ
hτυ : τ = υ ∨ τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ
have inl : ∀ (hστ : σ = τ), σ = υ ∨ σ = swap i j * υ
Tactic: rcases hστ with hστ | hστ
Cleared hypotheses: hστ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ ∨ σ = swap i j * τ
hτυ : τ = υ ∨ τ = swap i j * υ
inl : ∀ (hστ : σ = τ), σ = υ ∨ σ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ
have inr : ∀ (hστ : σ = swap i j * τ), σ = υ ∨ σ = swap i j * υ
Tactic: rcases hστ with hστ | hστ
Cleared hypotheses: hστ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hτυ : τ = υ ∨ τ = swap i j * υ
hστ : σ = τ
⊢ σ = υ ∨ σ = swap i j * υ
have inl : ∀ (hτυ : τ = υ), σ = υ ∨ σ = swap i j * υ
Tactic: rcases hτυ with hτυ | hτυ
Cleared hypotheses: hτυ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hτυ : τ = υ ∨ τ = swap i j * υ
hστ : σ = τ
inl : ∀ (hτυ : τ = υ), σ = υ ∨ σ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ
have inl₁ : ∀ (hτυ : τ = swap i j * υ), σ = υ ∨ σ = swap i j * υ
Tactic: rcases hτυ with hτυ | hτυ
Cleared hypotheses: hτυ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hτυ : τ = υ ∨ τ = swap i j * υ
hστ : σ = swap i j * τ
⊢ σ = υ ∨ σ = swap i j * υ
have inr : ∀ (hτυ : τ = υ), σ = υ ∨ σ = swap i j * υ
Tactic: rcases hτυ with hτυ | hτυ
Cleared hypotheses: hτυ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hτυ : τ = υ ∨ τ = swap i j * υ
hστ : σ = swap i j * τ
inr : ∀ (hτυ : τ = υ), σ = υ ∨ σ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ
have inr₁ : ∀ (hτυ : τ = swap i j * υ), σ = υ ∨ σ = swap i j * υ
Tactic: rcases hτυ with hτυ | hτυ
Cleared hypotheses: hτυ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ
have inr : υ = υ ∨ υ = swap i j * υ
Tactic: rw [hστ, hτυ, swap_mul_self_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ
have inr : υ = υ ∨ υ = swap i j * υ
Tactic: try rw [hστ, hτυ, swap_mul_self_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
x : α
⊢ Eq (α := α) ((List.prod [] : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
have rw : Eq (α := α) ((1 : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
Tactic: rw [List.prod_nil]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
m : { l : List (Perm α) // l.prod = swap x ((f : (a : α) → α) x) * f ∧ ∀ g ∈ l, g.IsSwap } :=
  swapFactorsAux l (swap x ((f : (a : α) → α) x) * f) ⋯
⊢ (swap x ((f : (a : α) → α) x) :: (↑m : List (Perm α))).prod = f
have rw : swap x ((f : (a : α) → α) x) * (↑m : List (Perm α)).prod = f
Tactic: rw [List.prod_cons, m.2.1, ← mul_assoc, mul_def (swap x (f x)), swap_swap, ← one_def,
          one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
m : { l : List (Perm α) // l.prod = swap x ((f : (a : α) → α) x) * f ∧ ∀ g ∈ l, g.IsSwap } :=
  swapFactorsAux l (swap x ((f : (a : α) → α) x) * f) ⋯
rw : swap x ((f : (a : α) → α) x) * (↑m : List (Perm α)).prod = f
⊢ (swap x ((f : (a : α) → α) x) :: (↑m : List (Perm α))).prod = f
have rw₁ : swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f) = f
Tactic: rw [List.prod_cons, m.2.1, ← mul_assoc, mul_def (swap x (f x)), swap_swap, ← one_def,
          one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
m : { l : List (Perm α) // l.prod = swap x ((f : (a : α) → α) x) * f ∧ ∀ g ∈ l, g.IsSwap } :=
  swapFactorsAux l (swap x ((f : (a : α) → α) x) * f) ⋯
rw : swap x ((f : (a : α) → α) x) * (↑m : List (Perm α)).prod = f
rw₁ : swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f) = f
⊢ (swap x ((f : (a : α) → α) x) :: (↑m : List (Perm α))).prod = f
have rw₂ : swap x ((f : (a : α) → α) x) * swap x ((f : (a : α) → α) x) * f = f
Tactic: rw [List.prod_cons, m.2.1, ← mul_assoc, mul_def (swap x (f x)), swap_swap, ← one_def,
          one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
m : { l : List (Perm α) // l.prod = swap x ((f : (a : α) → α) x) * f ∧ ∀ g ∈ l, g.IsSwap } :=
  swapFactorsAux l (swap x ((f : (a : α) → α) x) * f) ⋯
rw : swap x ((f : (a : α) → α) x) * (↑m : List (Perm α)).prod = f
rw₁ : swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f) = f
rw₂ : swap x ((f : (a : α) → α) x) * swap x ((f : (a : α) → α) x) * f = f
⊢ (swap x ((f : (a : α) → α) x) :: (↑m : List (Perm α))).prod = f
have rw₃ : Equiv.trans (swap x ((f : (a : α) → α) x)) (swap x ((f : (a : α) → α) x)) * f = f
Tactic: rw [List.prod_cons, m.2.1, ← mul_assoc, mul_def (swap x (f x)), swap_swap, ← one_def,
          one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
m : { l : List (Perm α) // l.prod = swap x ((f : (a : α) → α) x) * f ∧ ∀ g ∈ l, g.IsSwap } :=
  swapFactorsAux l (swap x ((f : (a : α) → α) x) * f) ⋯
rw : swap x ((f : (a : α) → α) x) * (↑m : List (Perm α)).prod = f
rw₁ : swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f) = f
rw₂ : swap x ((f : (a : α) → α) x) * swap x ((f : (a : α) → α) x) * f = f
rw₃ : Equiv.trans (swap x ((f : (a : α) → α) x)) (swap x ((f : (a : α) → α) x)) * f = f
⊢ (swap x ((f : (a : α) → α) x) :: (↑m : List (Perm α))).prod = f
have rw₄ : Equiv.refl α * f = f
Tactic: rw [List.prod_cons, m.2.1, ← mul_assoc, mul_def (swap x (f x)), swap_swap, ← one_def,
          one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
m : { l : List (Perm α) // l.prod = swap x ((f : (a : α) → α) x) * f ∧ ∀ g ∈ l, g.IsSwap } :=
  swapFactorsAux l (swap x ((f : (a : α) → α) x) * f) ⋯
rw : swap x ((f : (a : α) → α) x) * (↑m : List (Perm α)).prod = f
rw₁ : swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f) = f
rw₂ : swap x ((f : (a : α) → α) x) * swap x ((f : (a : α) → α) x) * f = f
rw₃ : Equiv.trans (swap x ((f : (a : α) → α) x)) (swap x ((f : (a : α) → α) x)) * f = f
rw₄ : Equiv.refl α * f = f
⊢ (swap x ((f : (a : α) → α) x) :: (↑m : List (Perm α))).prod = f
have rw₅ : 1 * f = f
Tactic: rw [List.prod_cons, m.2.1, ← mul_assoc, mul_def (swap x (f x)), swap_swap, ← one_def,
          one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
m : { l : List (Perm α) // l.prod = swap x ((f : (a : α) → α) x) * f ∧ ∀ g ∈ l, g.IsSwap } :=
  swapFactorsAux l (swap x ((f : (a : α) → α) x) * f) ⋯
rw : swap x ((f : (a : α) → α) x) * (↑m : List (Perm α)).prod = f
rw₁ : swap x ((f : (a : α) → α) x) * (swap x ((f : (a : α) → α) x) * f) = f
rw₂ : swap x ((f : (a : α) → α) x) * swap x ((f : (a : α) → α) x) * f = f
rw₃ : Equiv.trans (swap x ((f : (a : α) → α) x)) (swap x ((f : (a : α) → α) x)) * f = f
rw₄ : Equiv.refl α * f = f
rw₅ : 1 * f = f
⊢ (swap x ((f : (a : α) → α) x) :: (↑m : List (Perm α))).prod = f
have rw₆ : f = f
Tactic: rw [List.prod_cons, m.2.1, ← mul_assoc, mul_def (swap x (f x)), swap_swap, ← one_def,
          one_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
f : Perm α
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
⊢ motive f
have intro : ∀ (val : Fintype α), motive f
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
f : Perm α
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val : Fintype α
⊢ motive f
have intro : ∀ (l : List (Perm α)) (hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap), motive f
Tactic: obtain ⟨l, hl⟩ := (truncSwapFactors f).out
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val : Fintype α
g : Perm α
l : List (Perm α)
ih : ∀ (f : Perm α) (hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap), motive f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
⊢ motive f
have intro : ∀ (x y : α) (hxy : x ≠ y ∧ g = swap x y), motive f
Tactic: rcases hl.2 g (by simp) with ⟨x, y, hxy⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val : Fintype α
g : Perm α
l : List (Perm α)
ih : ∀ (f : Perm α) (hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap), motive f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
x y : α
hxy : x ≠ y ∧ g = swap x y
⊢ motive f
have intro : motive (swap x y * l.prod)
Tactic: rw [← hl.1, List.prod_cons, hxy.2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
f : Perm α
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val : Fintype α
l : List (Perm α)
hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap
⊢ motive f
have intro : ∀ (f : Perm α) (hl : List.prod [] = f ∧ ∀ (g : Perm α), Membership.mem (γ := List (Perm α)) [] g → g.IsSwap), motive f
Tactic: induction l generalizing f with
  | nil =>
    simp only [one, hl.left.symm, List.prod_nil]
  | cons g l ih =>
    rcases hl.2 g (by simp) with ⟨x, y, hxy⟩
    rw [← hl.1, List.prod_cons, hxy.2]
    exact swap_mul _ _ _ hxy.1 (ih _ ⟨rfl, fun v hv => hl.2 _ (List.mem_cons_of_mem _ hv)⟩)
Cleared hypotheses: f, l, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
motive : Perm α → Prop
f : Perm α
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val : Fintype α
l : List (Perm α)
hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap
intro :
  ∀ (f : Perm α) (hl : List.prod [] = f ∧ ∀ (g : Perm α), Membership.mem (γ := List (Perm α)) [] g → g.IsSwap), motive f
⊢ motive f
have intro₁ : ∀ (g : Perm α) (l : List (Perm α)) (ih : ∀ (f : Perm α) (hl : l.prod = f ∧ ∀ g ∈ l, g.IsSwap), motive f) (f : Perm α)
  (hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap), motive f
Tactic: induction l generalizing f with
  | nil =>
    simp only [one, hl.left.symm, List.prod_nil]
  | cons g l ih =>
    rcases hl.2 g (by simp) with ⟨x, y, hxy⟩
    rw [← hl.1, List.prod_cons, hxy.2]
    exact swap_mul _ _ _ hxy.1 (ih _ ⟨rfl, fun v hv => hl.2 _ (List.mem_cons_of_mem _ hv)⟩)
Cleared hypotheses: f, l, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
⊢ Eq.{u + 1} (α := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap}) ⊤
have intro : ∀ (val : Fintype α), Eq.{u + 1} (α := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap}) ⊤
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
val : Fintype α
⊢ Eq.{u + 1} (α := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap}) ⊤
have intro : ∀ (x : Perm α),
  Membership.mem (γ := Submonoid (Perm α)) ⊤ x →
    Membership.mem (γ := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap}) x
Tactic: refine top_unique fun x _ ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
val : Fintype α
x : Perm α
h : Membership.mem (γ := Submonoid (Perm α)) ⊤ x
⊢ Membership.mem (γ := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap}) x
have h1 : (↑(Trunc.out x.truncSwapFactors) : List (Perm α)).prod = x
Tactic: obtain ⟨h1, h2⟩ := (truncSwapFactors x).out.prop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
val : Fintype α
x : Perm α
h : Membership.mem (γ := Submonoid (Perm α)) ⊤ x
h1 : (↑(Trunc.out x.truncSwapFactors) : List (Perm α)).prod = x
⊢ Membership.mem (γ := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap}) x
have h2 : ∀ g ∈ (↑(Trunc.out x.truncSwapFactors) : List (Perm α)), g.IsSwap
Tactic: obtain ⟨h1, h2⟩ := (truncSwapFactors x).out.prop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
val : Fintype α
x : Perm α
h : Membership.mem (γ := Submonoid (Perm α)) ⊤ x
h1 : (↑(Trunc.out x.truncSwapFactors) : List (Perm α)).prod = x
h2 : ∀ g ∈ (↑(Trunc.out x.truncSwapFactors) : List (Perm α)), g.IsSwap
⊢ Membership.mem (γ := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap}) x
have intro : Membership.mem (γ := Submonoid (Perm α)) (Submonoid.closure {σ : Perm α | σ.IsSwap})
  (↑(Trunc.out x.truncSwapFactors) : List (Perm α)).prod
Tactic: rw [← h1]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
⊢ Eq (α := Submonoid (Perm (Fin (n + 1)))) (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) ⊤
have h : LE.le (α := Submonoid (Perm (Fin (n + 1)))) ⊤ (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ))
Tactic: apply top_unique
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
⊢ LE.le (α := Submonoid (Perm (Fin (n + 1)))) ⊤ (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ))
have h : {σ : Perm (Fin (n + 1)) | σ.IsSwap} ⊆
  (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
Tactic: rw [← mclosure_isSwap, Submonoid.closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
⊢ swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
have h : ∀
  (this :
    ∀ (i j : Fin (n + 1)) (ne : i ≠ j) (lt : i < j),
      swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1)))))
  (lt : ¬i < j),
  swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
Tactic: wlog lt : i < j generalizing i j
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
h :
  ∀
    (this :
      ∀ (i j : Fin (n + 1)) (ne : i ≠ j) (lt : i < j),
        swap i j ∈
          (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1)))))
    (lt : ¬i < j),
    swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
⊢ swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
have wlog : ∀ (i j : Fin (n + 1)) (ne : i ≠ j) (lt : i < j),
  swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
Tactic: wlog lt : i < j generalizing i j
Cleared hypotheses: i, j, ne
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this :
  ∀ (i j : Fin (n + 1)) (ne : i ≠ j) (lt : i < j),
    swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
lt : ¬i < j
⊢ swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
have h : swap j i ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
Tactic: rw [swap_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  ∀ (ne : i ≠ j.castSucc) (lt : i < j.castSucc),
    swap i j.castSucc ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
ne : i ≠ j.succ
lt : i < j.succ
⊢ swap i j.succ ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
have mem : Membership.mem (γ := Submonoid (Perm (Fin (n + 1))))
  (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) (swap j.castSucc j.succ)
Tactic: have mem : swap j.castSucc j.succ ∈ Submonoid.closure
      (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ) := Submonoid.subset_closure ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  ∀ (ne : i ≠ j.castSucc) (lt : i < j.castSucc),
    swap i j.castSucc ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
ne : i ≠ j.succ
lt : i < j.succ
mem :
  Membership.mem (γ := Submonoid (Perm (Fin (n + 1))))
    (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) (swap j.castSucc j.succ)
⊢ swap i j.succ ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
have succ : ∀
  (ih :
    ∀ (ne : j.castSucc ≠ j.castSucc) (lt : j.castSucc < j.castSucc),
      swap j.castSucc j.castSucc ∈
        (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1)))))
  (ne : j.castSucc ≠ j.succ) (lt : j.castSucc < j.succ),
  swap j.castSucc j.succ ∈
    (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
Tactic: obtain rfl | lts := (Fin.le_castSucc_iff.mpr lt).eq_or_lt
Cleared hypotheses: i, ih, ne, lt
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  ∀ (ne : i ≠ j.castSucc) (lt : i < j.castSucc),
    swap i j.castSucc ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
ne : i ≠ j.succ
lt : i < j.succ
mem :
  Membership.mem (γ := Submonoid (Perm (Fin (n + 1))))
    (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) (swap j.castSucc j.succ)
succ :
  ∀
    (ih :
      ∀ (ne : j.castSucc ≠ j.castSucc) (lt : j.castSucc < j.castSucc),
        swap j.castSucc j.castSucc ∈
          (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1)))))
    (ne : j.castSucc ≠ j.succ) (lt : j.castSucc < j.succ),
    swap j.castSucc j.succ ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
⊢ swap i j.succ ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
have succ₁ : ∀ (lts : i < j.castSucc),
  swap i j.succ ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
Tactic: obtain rfl | lts := (Fin.le_castSucc_iff.mpr lt).eq_or_lt
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  ∀ (ne : i ≠ j.castSucc) (lt : i < j.castSucc),
    swap i j.castSucc ∈
      (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
ne : i ≠ j.succ
lt : i < j.succ
mem :
  Membership.mem (γ := Submonoid (Perm (Fin (n + 1))))
    (Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) (swap j.castSucc j.succ)
lts : i < j.castSucc
⊢ swap i j.succ ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
have succ : swap j.castSucc j.succ * swap i j.castSucc * swap j.castSucc j.succ ∈
  (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
Tactic: rw [swap_comm, ← swap_mul_swap_mul_swap (y := Fin.castSucc j) lts.ne lt.ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
lt : i < j
⊢ swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
have zero : ∀ (ne : i ≠ 0) (lt : i < 0),
  swap i 0 ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
Tactic: induction j using Fin.induction with
  | zero => cases lt
  | succ j ih =>
    have mem : swap j.castSucc j.succ ∈ Submonoid.closure
      (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ) := Submonoid.subset_closure ⟨_, rfl⟩
    obtain rfl | lts := (Fin.le_castSucc_iff.mpr lt).eq_or_lt
    · exact mem
    rw [swap_comm, ← swap_mul_swap_mul_swap (y := Fin.castSucc j) lts.ne lt.ne]
    exact mul_mem (mul_mem mem <| ih lts.ne lts) mem
Cleared hypotheses: j, ne, lt
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
lt : i < j
zero :
  ∀ (ne : i ≠ 0) (lt : i < 0),
    swap i 0 ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
⊢ swap i j ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
have succ : ∀ (j : Fin n)
  (ih :
    ∀ (ne : i ≠ j.castSucc) (lt : i < j.castSucc),
      swap i j.castSucc ∈
        (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1)))))
  (ne : i ≠ j.succ) (lt : i < j.succ),
  swap i j.succ ∈ (↑(Submonoid.closure (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ)) : Set (Perm (Fin (n + 1))))
Tactic: induction j using Fin.induction with
  | zero => cases lt
  | succ j ih =>
    have mem : swap j.castSucc j.succ ∈ Submonoid.closure
      (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ) := Submonoid.subset_closure ⟨_, rfl⟩
    obtain rfl | lts := (Fin.le_castSucc_iff.mpr lt).eq_or_lt
    · exact mem
    rw [swap_comm, ← swap_mul_swap_mul_swap (y := Fin.castSucc j) lts.ne lt.ne]
    exact mul_mem (mul_mem mem <| ih lts.ne lts) mem
Cleared hypotheses: j, ne, lt