awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (goal)
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
⊢ Trunc (P (ULift.{u, 0} (Fin n)))
have zero : Trunc (P (ULift.{u, 0} (Fin 0)))
Tactic: induction n with
  | zero =>
    have : card PEmpty = card (ULift (Fin 0)) := by
      simp only [card_fin, card_pempty, card_ulift]
    apply Trunc.bind (truncEquivOfCardEq this)
    intro e
    apply Trunc.mk
    exact of_equiv e h_empty
  | succ n ih =>
    have : card (Option (ULift (Fin n))) = card (ULift (Fin n.succ)) := by
      simp only [card_fin, card_option, card_ulift]
    apply Trunc.bind (truncEquivOfCardEq this)
    intro e
    apply Trunc.map _ ih
    intro ih
    exact of_equiv e (h_option ih)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (goal)
Goal:
α_1 : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
zero : Trunc (P (ULift.{u, 0} (Fin 0)))
⊢ Trunc (P (ULift.{u, 0} (Fin n)))
have succ : (n : ℕ) → (ih : Trunc (P (ULift.{u, 0} (Fin n)))) → Trunc (P (ULift.{u, 0} (Fin (n + 1))))
Tactic: induction n with
  | zero =>
    have : card PEmpty = card (ULift (Fin 0)) := by
      simp only [card_fin, card_pempty, card_ulift]
    apply Trunc.bind (truncEquivOfCardEq this)
    intro e
    apply Trunc.mk
    exact of_equiv e h_empty
  | succ n ih =>
    have : card (Option (ULift (Fin n))) = card (ULift (Fin n.succ)) := by
      simp only [card_fin, card_option, card_ulift]
    apply Trunc.bind (truncEquivOfCardEq this)
    intro e
    apply Trunc.map _ ih
    intro ih
    exact of_equiv e (h_option ih)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (hypothesis)
Goal:
P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
⊢ P α
have x : Trunc (∀ (h : Fintype α), P α)
Tactic: obtain ⟨p⟩ :=
    let f_empty := fun i => by convert! h_empty
    let h_option : ∀ {α : Type u} [Fintype α] [DecidableEq α],
          (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α) := by
      rintro α hα - Pα hα'
      convert! h_option α (Pα _)
    @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
      f_empty h_option α _ (Classical.decEq α)
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (hypothesis)
Goal:
P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
x : Trunc (∀ (h : Fintype α), P α)
⊢ P α
have p : ∀ (h : Fintype α), P α
Tactic: obtain ⟨p⟩ :=
    let f_empty := fun i => by convert! h_empty
    let h_option : ∀ {α : Type u} [Fintype α] [DecidableEq α],
          (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α) := by
      rintro α hα - Pα hα'
      convert! h_option α (Pα _)
    @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
      f_empty h_option α _ (Classical.decEq α)
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (goal)
Goal:
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst : Finite α
⊢ P α
have intro : ∀ (val : Fintype α), P α
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Data.Fintype.Option (goal)
Goal:
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst : Finite α
val : Fintype α
⊢ P α
have intro : ∀ (α β : Type u) [Fintype β] (e : α ≃ β), P α → P β
Tactic: refine Fintype.induction_empty_option ?_ ?_ ?_ α
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
have h : Eq (α := α) (⨆ b ∈ s, a ⊓ b) (s.toFinset.sup fun (i : α) ↦ a ⊓ id i)
Tactic: convert! (Finset.sup_inf_distrib_left s.toFinset id a).le using 1
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
⊢ Eq (α := α) (⨆ b ∈ s, a ⊓ b) (s.toFinset.sup fun (i : α) ↦ a ⊓ id i)
have h : Eq.{u_2 + 1} (α := α) (⨆ b ∈ s, a ⊓ b) (⨆ a_1 ∈ s.toFinset, a ⊓ id a_1)
Tactic: rw [Finset.sup_eq_iSup]
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
⊢ Eq.{u_2 + 1} (α := α) (⨆ b ∈ s, a ⊓ b) (⨆ a_1 ∈ s.toFinset, a ⊓ id a_1)
have h : Eq.{u_2 + 1} (α := α) (⨆ b ∈ s, a ⊓ b) (⨆ a_1 ∈ s, a ⊓ id a_1)
Tactic: simp_rw [Set.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
have h : Eq (α := α) (⨅ b ∈ s, a ⊔ b) (s.toFinset.inf fun (i : α) ↦ a ⊔ id i)
Tactic: convert! (Finset.inf_sup_distrib_left s.toFinset id a).ge using 1
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
⊢ Eq (α := α) (⨅ b ∈ s, a ⊔ b) (s.toFinset.inf fun (i : α) ↦ a ⊔ id i)
have h : Eq.{u_2 + 1} (α := α) (⨅ b ∈ s, a ⊔ b) (⨅ a_1 ∈ s.toFinset, a ⊔ id a_1)
Tactic: rw [Finset.inf_eq_iInf]
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype ι
inst_1 : Fintype α
inst_2 : DistribLattice α
inst_3 : BoundedOrder α
a : α
s : Set α
⊢ Eq.{u_2 + 1} (α := α) (⨅ b ∈ s, a ⊔ b) (⨅ a_1 ∈ s.toFinset, a ⊔ id a_1)
have h : Eq.{u_2 + 1} (α := α) (⨅ b ∈ s, a ⊔ b) (⨅ a_1 ∈ s, a ⊔ id a_1)
Tactic: simp_rw [Set.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
γ : Type u_3
inst_1 : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
⊢ ∃ (z : γ), ∀ i ∈ s, r (f i) (f z)
have h : ∀ (x a : γ), a ∈ s → r (f a) (f x) ↔ a ∈ hs.toFinset (s := s) → r (f a) (f x)
Tactic: convert! D.finset_le hs.toFinset using 3
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
γ : Type u_3
inst_1 : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
x a : γ
⊢ a ∈ s → r (f a) (f x) ↔ a ∈ hs.toFinset (s := s) → r (f a) (f x)
have h : a ∈ s → r (f a) (f x) ↔ a ∈ s → r (f a) (f x)
Tactic: rw [Set.Finite.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsDirectedOrder α
f : β → α
⊢ BddAbove (Set.range f)
have obtain : ∀ (M : α) (hM : ∀ (i : β), f i ≤ M), BddAbove (Set.range f)
Tactic: obtain ⟨M, hM⟩ := Finite.exists_le f
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsDirectedOrder α
f : β → α
M : α
hM : ∀ (i : β), f i ≤ M
⊢ BddAbove (Set.range f)
have refine : ∀ (a : α) (ha : a ∈ Set.range f), a ≤ M
Tactic: refine ⟨M, fun a ha => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsCodirectedOrder α
f : β → α
⊢ BddBelow (Set.range f)
have obtain : ∀ (M : α) (hM : ∀ (i : β), M ≤ f i), BddBelow (Set.range f)
Tactic: obtain ⟨M, hM⟩ := Finite.exists_ge f
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
inst_1 : Nonempty α
inst_2 : Preorder α
inst_3 : IsCodirectedOrder α
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
⊢ BddBelow (Set.range f)
have refine : ∀ (a : α) (ha : a ∈ Set.range f), M ≤ a
Tactic: refine ⟨M, fun a ha => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → α
inst_1 : Nonempty ι
inst_2 : Finite ι
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
ha : a ≤ ⨆ (i : ι), f i
⊢ ∃ (i : ι), a ≤ f i
have obtain : ∀ (i : ι) (hi : ∀ (i_1 : ι), f (id i_1) ≤ f i), ∃ (i : ι), a ≤ f i
Tactic: obtain ⟨i, hi⟩ := hf.finite_le id
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
a : α
hs : s.Nonempty
hs' : s.Finite
hs'' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ a ≤ sSup s ↔ ∃ b ∈ s, a ≤ b
have this : Nonempty.{u_2 + 1} (↑s : Type u_2)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
a : α
hs : s.Nonempty
hs' : s.Finite
hs'' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
⊢ a ≤ sSup s ↔ ∃ b ∈ s, a ≤ b
have this₁ : Finite.{u_2 + 1} (↑s : Type u_2)
Tactic: have := hs'.to_subtype
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Nonempty ι
f : ι → α
a : α
⊢ (⨆ (i : ι), f i) ⊔ a = ⨆ (i : ι), f i ⊔ a
have refine_1 : LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), f i ⊔ a)
Tactic: refine le_antisymm (sup_le ?_ ?_) <| ciSup_le fun i ↦ sup_le_sup_right (le_ciSup f i) a
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : ConditionallyCompleteLattice α
inst_2 : Nonempty ι
f : ι → α
a : α
refine_1 : LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), f i ⊔ a)
⊢ (⨆ (i : ι), f i) ⊔ a = ⨆ (i : ι), f i ⊔ a
have refine_2 : a ≤ ⨆ (i : ι), f i ⊔ a
Tactic: refine le_antisymm (sup_le ?_ ?_) <| ciSup_le fun i ↦ sup_le_sup_right (le_ciSup f i) a
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
⊢ g (⨆ (i : ι), f i) = ⨆ (i : ι), g (f i)
have obtain : ∀ (j : ι) (hj : f j = ⨆ (i : ι), f i), g (⨆ (i : ι), f i) = ⨆ (i : ι), g (f i)
Tactic: obtain ⟨j, hj⟩ : ∃ j, f j = ⨆ i, f i := exists_eq_ciSup_of_finite
-- Lean 4 proof step from Mathlib.Data.Fintype.Order (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Finite ι
inst_3 : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
j : ι
hj : f j = ⨆ (i : ι), f i
⊢ g (⨆ (i : ι), f i) = ⨆ (i : ι), g (f i)
have rw : g (f j) = ⨆ (i : ι), g (f i)
Tactic: rw [← hj]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
⊢ Membership.mem (γ := List (Equiv.Perm α)) (permsOfList []) f
have h₁ : ∀ (x : α), (f : (a : α) → α) x ≠ x → False
Tactic: simp only [not_mem_nil] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
⊢ f ∈ permsOfList (a :: l)
have pos : ∀ (hfa : (f : (a : α) → α) a = a), f ∈ permsOfList (a :: l)
Tactic: by_cases hfa : f a = a
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
pos : ∀ (hfa : (f : (a : α) → α) a = a), f ∈ permsOfList (a :: l)
⊢ f ∈ permsOfList (a :: l)
have neg : ∀ (hfa : ¬(f : (a : α) → α) a = a), f ∈ permsOfList (a :: l)
Tactic: by_cases hfa : f a = a
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : (f : (a : α) → α) a = a
⊢ f ∈ permsOfList (a :: l)
have pos : ∀ (x : α) (hx : (f : (a : α) → α) x ≠ x), x ≠ a
Tactic: refine mem_append_left _ (IH fun x hx => mem_of_ne_of_mem ?_ (h x hx))
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
⊢ f ∈ permsOfList (a :: l)
have hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
Tactic: have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
x : α
h : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : ¬(f : (a : α) → α) x = x
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
hx : (Equiv.swap x ((f : (a : α) → α) x) * f : (a : α) → α) x ≠ x
⊢ False
have apply : (Equiv.swap x ((f : (a : α) → α) x) * f : (a : α) → α) x = x
Tactic: apply hx
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
x : α
hx : (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x
⊢ x ∈ l
have hxa : x ≠ a
Tactic: have hxa : x ≠ a := by
      rintro rfl
      apply hx
      simp only [mul_apply, swap_apply_right]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
x : α
hx : (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x
hxa : x ≠ a
⊢ x ∈ l
have refine : ∀ (h : (f : (a : α) → α) x = x), False
Tactic: refine List.mem_of_ne_of_mem hxa (h x fun h => ?_)
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h_1 : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
x : α
hx : (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x
hxa : x ≠ a
h : (f : (a : α) → α) x = x
⊢ False
have hx₁ : ¬(if (f : (a : α) → α) x = a then (f : (a : α) → α) a else if x = a then a else (f : (a : α) → α) x) = x
Tactic: simp only [mul_apply, swap_apply_def, mul_apply, Ne, apply_eq_iff_eq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h_1 : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
x : α
hxa : x ≠ a
h : (f : (a : α) → α) x = x
hx : ¬(if (f : (a : α) → α) x = a then (f : (a : α) → α) a else if x = a then a else (f : (a : α) → α) x) = x
⊢ False
have pos : ∀ (h_1 : (f : (a : α) → α) x = a) (hx : ¬(f : (a : α) → α) a = x), False
Tactic: split_ifs at hx with h_1
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h_1 : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
x : α
hxa : x ≠ a
h : (f : (a : α) → α) x = x
hx : ¬(if (f : (a : α) → α) x = a then (f : (a : α) → α) a else if x = a then a else (f : (a : α) → α) x) = x
pos : ∀ (h_1 : (f : (a : α) → α) x = a) (hx : ¬(f : (a : α) → α) a = x), False
⊢ False
have neg : ∀ (h_1 : ¬(f : (a : α) → α) x = a) (hx : ¬(f : (a : α) → α) x = x), False
Tactic: split_ifs at hx with h_1
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
⊢ f ∈ permsOfList (a :: l)
have this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
Tactic: have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l := by
    intro x hx
    have hxa : x ≠ a := by
      rintro rfl
      apply hx
      simp only [mul_apply, swap_apply_right]
    refine List.mem_of_ne_of_mem hxa (h x fun h => ?_)
    simp only [mul_apply, swap_apply_def, mul_apply, Ne, apply_eq_iff_eq] at hx
    split_ifs at hx with h_1
    exacts [hxa (h.symm.trans h_1), hx h]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
⊢ f ∈ permsOfList (a :: l)
have neg : f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f
Tactic: suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by
    simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_flatMap]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
⊢ f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f
have neg : ∀ (_hfl : f ∉ permsOfList l), Membership.mem (α := α) l ((f : (a : α) → α) a : α)
Tactic: refine or_iff_not_imp_left.2 fun _hfl => ⟨f a, ?_, Equiv.swap a (f a) * f, IH this, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
neg : ∀ (_hfl : f ∉ permsOfList l), Membership.mem (α := α) l ((f : (a : α) → α) a : α)
⊢ f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f
have neg₁ : ∀ (_hfl : f ∉ permsOfList l), Equiv.swap a ((f : (a : α) → α) a) * (Equiv.swap a ((f : (a : α) → α) a) * f) = f
Tactic: refine or_iff_not_imp_left.2 fun _hfl => ⟨f a, ?_, Equiv.swap a (f a) * f, IH this, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
⊢ Equiv.swap a ((f : (a : α) → α) a) * (Equiv.swap a ((f : (a : α) → α) a) * f) = f
have neg : Equiv.swap a ((f : (a : α) → α) a) * Equiv.swap a ((f : (a : α) → α) a) * f = f
Tactic: rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
neg : Equiv.swap a ((f : (a : α) → α) a) * Equiv.swap a ((f : (a : α) → α) a) * f = f
⊢ Equiv.swap a ((f : (a : α) → α) a) * (Equiv.swap a ((f : (a : α) → α) a) * f) = f
have neg₁ : Equiv.trans (Equiv.swap a ((f : (a : α) → α) a)) (Equiv.swap a ((f : (a : α) → α) a)) * f = f
Tactic: rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
neg : Equiv.swap a ((f : (a : α) → α) a) * Equiv.swap a ((f : (a : α) → α) a) * f = f
neg₁ : Equiv.trans (Equiv.swap a ((f : (a : α) → α) a)) (Equiv.swap a ((f : (a : α) → α) a)) * f = f
⊢ Equiv.swap a ((f : (a : α) → α) a) * (Equiv.swap a ((f : (a : α) → α) a) * f) = f
have neg₂ : Equiv.refl α * f = f
Tactic: rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]