awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
b : Perm α
hb : Membership.mem (γ := Subgroup (Perm α)) (closure T) b
⊢ _root_.Disjoint a.support b.support
have key1 : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
Tactic: have key1 := support_closure_subset_union S a ha
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
b : Perm α
hb : Membership.mem (γ := Subgroup (Perm α)) (closure T) b
key1 : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
⊢ _root_.Disjoint a.support b.support
have key2 : (↑b.support : Set α) ⊆ ⋃ b ∈ T, (↑b.support : Set α)
Tactic: have key2 := support_closure_subset_union T b hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
b : Perm α
hb : Membership.mem (γ := Subgroup (Perm α)) (closure T) b
key1 : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
key2 : (↑b.support : Set α) ⊆ ⋃ b ∈ T, (↑b.support : Set α)
⊢ _root_.Disjoint a.support b.support
have key : ∀ (h : _root_.Disjoint.{u} (α := Set α) (⋃ b ∈ S, (↑b.support : Set α)) (⋃ b ∈ T, (↑b.support : Set α))),
  _root_.Disjoint (↑a.support : Set α) (↑b.support : Set α)
Tactic: have key := Set.disjoint_of_subset key1 key2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
b : Perm α
hb : Membership.mem (γ := Subgroup (Perm α)) (closure T) b
key1 : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
key2 : (↑b.support : Set α) ⊆ ⋃ b ∈ T, (↑b.support : Set α)
key :
  ∀ (h : _root_.Disjoint.{u} (α := Set α) (⋃ b ∈ S, (↑b.support : Set α)) (⋃ b ∈ T, (↑b.support : Set α))),
    _root_.Disjoint (↑a.support : Set α) (↑b.support : Set α)
⊢ _root_.Disjoint a.support b.support
have key₁ : ∀ (h : ∀ (i : Perm α) (i_1 : i ∈ S) (i_2 : Perm α) (i_3 : i_2 ∈ T), _root_.Disjoint i.support i_2.support),
  _root_.Disjoint a.support b.support
Tactic: simp_rw [Set.disjoint_iUnion_left, Set.disjoint_iUnion_right, Finset.disjoint_coe] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ _root_.Disjoint (α := Subgroup (Perm α)) (closure S) (closure T)
have h₁ : ∀ (a : Perm α),
  Membership.mem (γ := Subgroup (Perm α)) (closure S) a →
    ∀ (b : Perm α), Membership.mem (γ := Subgroup (Perm α)) (closure T) b → _root_.Disjoint a.support b.support
Tactic: apply disjoint_of_disjoint_support
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
⊢ Membership.mem (γ := Subgroup (Perm α)) (MonoidHom.range (G := Perm (Subtype p)) (ofSubtype (p := p))) g ↔
    (↑g.support : Set α) ⊆ setOf p
have mp : Membership.mem (γ := Subgroup (Perm α)) (MonoidHom.range (G := Perm (Subtype p)) (ofSubtype (p := p))) g →
  (↑g.support : Set α) ⊆ setOf p
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
mp :
  Membership.mem (γ := Subgroup (Perm α)) (MonoidHom.range (G := Perm (Subtype p)) (ofSubtype (p := p))) g →
    (↑g.support : Set α) ⊆ setOf p
⊢ Membership.mem (γ := Subgroup (Perm α)) (MonoidHom.range (G := Perm (Subtype p)) (ofSubtype (p := p))) g ↔
    (↑g.support : Set α) ⊆ setOf p
have mpr : (↑g.support : Set α) ⊆ setOf p →
  Membership.mem (γ := Subgroup (Perm α)) (MonoidHom.range (G := Perm (Subtype p)) (ofSubtype (p := p))) g
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
k : Perm (Subtype p)
x : α
⊢ x ∈ (↑(support ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) k)) : Set α) → x ∈ setOf p
have mp : (∃ (hx : p x), Subtype.mk (p := p) x hx ∈ k.support) → p x
Tactic: simp only [Finset.mem_coe, mem_support_ofSubtype, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
⊢ Membership.mem (γ := Subgroup (Perm α)) (MonoidHom.range (G := Perm (Subtype p)) (ofSubtype (p := p))) g
have mpr : ∀ (x : α), p ((g : (a : α) → α) x) ↔ p x
Tactic: refine ⟨g.subtypePerm fun x ↦ ?_, ofSubtype_subtypePerm _ fun x hx ↦ hg (mem_support.mpr hx)⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
x : α
⊢ p ((g : (a : α) → α) x) ↔ p x
have pos : ∀ (hx : (g : (a : α) → α) x = x), p ((g : (a : α) → α) x) ↔ p x
Tactic: by_cases hx : g x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
x : α
pos : ∀ (hx : (g : (a : α) → α) x = x), p ((g : (a : α) → α) x) ↔ p x
⊢ p ((g : (a : α) → α) x) ↔ p x
have neg : ∀ (hx : ¬(g : (a : α) → α) x = x), p ((g : (a : α) → α) x) ↔ p x
Tactic: by_cases hx : g x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
x : α
hx : (g : (a : α) → α) x = x
⊢ p ((g : (a : α) → α) x) ↔ p x
have pos : p x ↔ p x
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
x : α
hx : ¬(g : (a : α) → α) x = x
⊢ p ((g : (a : α) → α) x) ↔ p x
have neg : Membership.mem (α := α) (↑g.support : Set α) ((g : (a : α) → α) x : α)
Tactic: refine iff_of_true (hg ?_) (hg ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Finite (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
x : α
hx : ¬(g : (a : α) → α) x = x
neg : Membership.mem (α := α) (↑g.support : Set α) ((g : (a : α) → α) x : α)
⊢ p ((g : (a : α) → α) x) ↔ p x
have neg₁ : x ∈ (↑g.support : Set α)
Tactic: refine iff_of_true (hg ?_) (hg ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith swap l l').prod.support
⊢ x ∈ l.toFinset ⊔ l'.toFinset
have hx' : Membership.mem (γ := Set α) {x : α | ((zipWith swap l l').prod : (a : α) → α) x ≠ x} x
Tactic: have hx' : x ∈ { x | (zipWith swap l l').prod x ≠ x } := by simpa using hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ {x : α | (l.formPerm : (a : α) → α) x ≠ x} ≤ (↑l.toFinset : Set α)
have refine : (↑(l.toFinset ⊔ l.tail.toFinset) : Set α) ≤ (↑l.toFinset : Set α)
Tactic: refine (zipWith_swap_prod_support' l l.tail).trans ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
inst_1 : Fintype α
x : α
hx : x ∈ l.formPerm.support
⊢ x ∈ l.toFinset
have hx' : Membership.mem (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x} x
Tactic: have hx' : x ∈ { x | formPerm l x ≠ x } := by simpa using hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : x ∈ l
⊢ Membership.mem (α := α) l ((l.formPerm : (a : α) → α) x : α)
have nil : ∀ (h : Membership.mem (γ := List α) [] x), Membership.mem (α := α) (γ := List α) [] ((formPerm [] : (a : α) → α) x : α)
Tactic: rcases l with - | ⟨y, l⟩
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : x ∈ l
nil :
  ∀ (h : Membership.mem (γ := List α) [] x),
    Membership.mem (α := α) (γ := List α) [] ((formPerm [] : (a : α) → α) x : α)
⊢ Membership.mem (α := α) l ((l.formPerm : (a : α) → α) x : α)
have cons : ∀ (y : α) (l : List α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
Tactic: rcases l with - | ⟨y, l⟩
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
⊢ Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)
have pos : ∀ (hx : x ∈ z :: l), Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)
Tactic: by_cases hx : x ∈ z :: l
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
pos : ∀ (hx : x ∈ z :: l), Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)
⊢ Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)
have neg : ∀ (hx : x ∉ z :: l), Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)
Tactic: by_cases hx : x ∈ z :: l
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
⊢ Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)
have pos : (if ((z :: l).formPerm : (a : α) → α) x = y then z
  else if ((z :: l).formPerm : (a : α) → α) x = z then y else ((z :: l).formPerm : (a : α) → α) x) ∈
  y :: z :: l
Tactic: rw [formPerm_cons_cons, mul_apply, swap_apply_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
⊢ (if ((z :: l).formPerm : (a : α) → α) x = y then z
    else if ((z :: l).formPerm : (a : α) → α) x = z then y else ((z :: l).formPerm : (a : α) → α) x) ∈
    y :: z :: l
have pos : ((z :: l).formPerm : (a : α) → α) x = y → z ∈ y :: z :: l
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
pos : ((z :: l).formPerm : (a : α) → α) x = y → z ∈ y :: z :: l
⊢ (if ((z :: l).formPerm : (a : α) → α) x = y then z
    else if ((z :: l).formPerm : (a : α) → α) x = z then y else ((z :: l).formPerm : (a : α) → α) x) ∈
    y :: z :: l
have pos₁ : ¬((z :: l).formPerm : (a : α) → α) x = y → ((z :: l).formPerm : (a : α) → α) x = z → y ∈ y :: z :: l
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
pos : ((z :: l).formPerm : (a : α) → α) x = y → z ∈ y :: z :: l
pos₁ : ¬((z :: l).formPerm : (a : α) → α) x = y → ((z :: l).formPerm : (a : α) → α) x = z → y ∈ y :: z :: l
⊢ (if ((z :: l).formPerm : (a : α) → α) x = y then z
    else if ((z :: l).formPerm : (a : α) → α) x = z then y else ((z :: l).formPerm : (a : α) → α) x) ∈
    y :: z :: l
have neg : ¬((z :: l).formPerm : (a : α) → α) x = y →
  ¬((z :: l).formPerm : (a : α) → α) x = z →
    Membership.mem (α := α) (y :: z :: l) (((z :: l).formPerm : (a : α) → α) x : α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
hx : x ∉ z :: l
⊢ Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)
have h₁ : x = y
Tactic: replace h : x = y := Or.resolve_right (mem_cons.1 h) hx
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
l : List α
h : x ∈ y :: l
⊢ Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
have cons : ∀ {x : α} (y : α) (h : x ∈ [y]), Membership.mem (α := α) [y] (([y].formPerm : (a : α) → α) x : α)
Tactic: induction l generalizing x y with
  | nil => simpa using h
  | cons z l IH =>
    by_cases hx : x ∈ z :: l
    · rw [formPerm_cons_cons, mul_apply, swap_apply_def]
      split_ifs
      · simp
      · simp
      · simp [*]
    · replace h : x = y := Or.resolve_right (mem_cons.1 h) hx
      simp [formPerm_apply_of_notMem hx, ← h]
Cleared hypotheses: x, y, l, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
l : List α
h : x ∈ y :: l
cons : ∀ {x : α} (y : α) (h : x ∈ [y]), Membership.mem (α := α) [y] (([y].formPerm : (a : α) → α) x : α)
⊢ Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
have cons₁ : ∀ (z : α) (l : List α)
  (IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α))
  {x : α} (y : α) (h : x ∈ y :: z :: l),
  Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)
Tactic: induction l generalizing x y with
  | nil => simpa using h
  | cons z l IH =>
    by_cases hx : x ∈ z :: l
    · rw [formPerm_cons_cons, mul_apply, swap_apply_def]
      split_ifs
      · simp
      · simp
      · simp [*]
    · replace h : x = y := Or.resolve_right (mem_cons.1 h) hx
      simp [formPerm_apply_of_notMem hx, ← h]
Cleared hypotheses: x, y, l, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : Membership.mem (α := α) l ((l.formPerm : (a : α) → α) x : α)
⊢ x ∈ l
have contrapose : ∀ (h : x ∉ l), ((l.formPerm : (a : α) → α) x : α) ∉ l
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
xs : List α
⊢ ((x :: (xs ++ [y])).formPerm : (a : α) → α) y = x
have nil : ∀ (x y : α), ((x :: ([] ++ [y])).formPerm : (a : α) → α) y = x
Tactic: induction xs generalizing x y with
  | nil => simp
  | cons z xs IH => simp [IH]
Cleared hypotheses: x, y, xs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
xs : List α
nil : ∀ (x y : α), ((x :: ([] ++ [y])).formPerm : (a : α) → α) y = x
⊢ ((x :: (xs ++ [y])).formPerm : (a : α) → α) y = x
have cons : ∀ (z : α) (xs : List α) (IH : ∀ (x y : α), ((x :: (xs ++ [y])).formPerm : (a : α) → α) y = x) (x y : α),
  ((x :: (z :: xs ++ [y])).formPerm : (a : α) → α) y = x
Tactic: induction xs generalizing x y with
  | nil => simp
  | cons z xs IH => simp [IH]
Cleared hypotheses: x, y, xs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
⊢ ((x :: xs).formPerm : (a : α) → α) ((x :: xs).getLast ⋯) = x
have nil : ∀ (x : α), ([x].formPerm : (a : α) → α) ([x].getLast sorry) = x
Tactic: induction xs using List.reverseRecOn generalizing x
Cleared hypotheses: x, xs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
nil : ∀ (x : α), ([x].formPerm : (a : α) → α) ([x].getLast ⋯) = x
⊢ ((x :: xs).formPerm : (a : α) → α) ((x :: xs).getLast ⋯) = x
have append_singleton : ∀ (l : List α) (a : α),
  (∀ (x : α), ((x :: l).formPerm : (a : α) → α) ((x :: l).getLast sorry) = x) →
    ∀ (x : α), ((x :: (l ++ [a])).formPerm : (a : α) → α) ((x :: (l ++ [a])).getLast sorry) = x
Tactic: induction xs using List.reverseRecOn generalizing x
Cleared hypotheses: x, xs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
⊢ ((x :: xs).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) xs.length ⋯) =
    x
have rw : ((x :: xs).formPerm : (a : α) → α) ((x :: xs).getLast sorry) = x
Tactic: rw [getElem_cons_length rfl, formPerm_apply_getLast]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
rw : ((x :: xs).formPerm : (a : α) → α) ((x :: xs).getLast ⋯) = x
⊢ ((x :: xs).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) xs.length ⋯) =
    x
have rw₁ : x = x
Tactic: rw [getElem_cons_length rfl, formPerm_apply_getLast]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
hl : 1 < l.length
⊢ (l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 1 hl
have nil : ∀ (h : Nodup.{u_1} (α := α) []) (hl : 1 < length.{u_1} (α := α) []),
  (formPerm [] : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 sorry) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 1 hl
Tactic: rcases l with (_ | ⟨x, _ | ⟨y, tl⟩⟩)
Cleared hypotheses: l, h, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
hl : 1 < l.length
nil :
  ∀ (h : Nodup.{u_1} (α := α) []) (hl : 1 < length.{u_1} (α := α) []),
    (formPerm [] : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 1 hl
⊢ (l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 1 hl
have cons : ∀ (x : α) (h : [x].Nodup) (hl : 1 < [x].length),
  ([x].formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] 0 sorry) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] 1 hl
Tactic: rcases l with (_ | ⟨x, _ | ⟨y, tl⟩⟩)
Cleared hypotheses: l, h, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
hl : 1 < l.length
nil :
  ∀ (h : Nodup.{u_1} (α := α) []) (hl : 1 < length.{u_1} (α := α) []),
    (formPerm [] : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 1 hl
cons :
  ∀ (x : α) (h : [x].Nodup) (hl : 1 < [x].length),
    ([x].formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] 0 ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] 1 hl
⊢ (l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 1 hl
have cons₁ : ∀ (x y : α) (tl : List α) (h : (x :: y :: tl).Nodup) (hl : 1 < (x :: y :: tl).length),
  ((x :: y :: tl).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 0 sorry) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
Tactic: rcases l with (_ | ⟨x, _ | ⟨y, tl⟩⟩)
Cleared hypotheses: l, h, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
tl : List α
h : (x :: y :: tl).Nodup
hl : 1 < (x :: y :: tl).length
⊢ ((x :: y :: tl).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 0 ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
have cons : ((x :: y :: tl).formPerm : (a : α) → α) x =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
Tactic: rw [getElem_cons_zero, formPerm_apply_head _ _ _ h, getElem_cons_succ, getElem_cons_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
tl : List α
h : (x :: y :: tl).Nodup
hl : 1 < (x :: y :: tl).length
cons :
  ((x :: y :: tl).formPerm : (a : α) → α) x =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
⊢ ((x :: y :: tl).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 0 ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
have cons₁ : y = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
Tactic: rw [getElem_cons_zero, formPerm_apply_head _ _ _ h, getElem_cons_succ, getElem_cons_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
tl : List α
h : (x :: y :: tl).Nodup
hl : 1 < (x :: y :: tl).length
cons :
  ((x :: y :: tl).formPerm : (a : α) → α) x =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
cons₁ : y = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
⊢ ((x :: y :: tl).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 0 ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
have cons₂ : y = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tl) 0 sorry
Tactic: rw [getElem_cons_zero, formPerm_apply_head _ _ _ h, getElem_cons_succ, getElem_cons_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
tl : List α
h : (x :: y :: tl).Nodup
hl : 1 < (x :: y :: tl).length
cons :
  ((x :: y :: tl).formPerm : (a : α) → α) x =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
cons₁ : y = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
cons₂ : y = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tl) 0 ⋯
⊢ ((x :: y :: tl).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 0 ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
have cons₃ : y = y
Tactic: rw [getElem_cons_zero, formPerm_apply_head _ _ _ h, getElem_cons_succ, getElem_cons_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.List (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y : α
⊢ ((y :: l).formPerm : (a : α) → α) x = y ↔
    Eq (α := α) (((y :: l).formPerm : (a : α) → α) x : α) (((y :: l).formPerm : (a : α) → α) ((y :: l).getLast ⋯) : α)
have rw : ((y :: l).formPerm : (a : α) → α) x = y ↔ ((y :: l).formPerm : (a : α) → α) x = y
Tactic: rw [formPerm_apply_getLast]