awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
a_1 : Sym2 α
a b : α
⊢ Quot.mk (Sym2.Rel α) (a, b) ∈ s.sym2 ↔ Quot.mk (Sym2.Rel α) (a, b) ∈ image (Function.uncurry Sym2.mk) (s ×ˢ s)
have h : a ∈ s ∧ b ∈ s ↔ ∃ (a_2 : α) (b_1 : α), (a_2 ∈ s ∧ b_1 ∈ s) ∧ (a_2 = a ∧ b_1 = b ∨ a_2 = b ∧ b_1 = a)
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
a b : α
h : (a, b) ∈ s.diag
⊢ s(a, b).IsDiag
have simp : ∀ (h : a ∈ s ∧ a = b), a = b
Tactic: simp at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
a b : α
h : (a, b) ∈ s.offDiag
⊢ ¬s(a, b).IsDiag
have simp : ∀ (h : a ∈ s ∧ b ∈ s ∧ ¬a = b), ¬a = b
Tactic: simp at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
a : α
⊢ (∀ b ∈ Sym2.diag a, b ∈ s) ↔ a ∈ s
have rw : Sym2.diag a ∈ s.sym2 ↔ a ∈ s
Tactic: rw [← mem_sym2_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ image (Function.uncurry Sym2.mk) s.diag ∪ image (Function.uncurry Sym2.mk) s.offDiag = s.sym2
have rw : image (Function.uncurry Sym2.mk) (s.diag ∪ s.offDiag) = s.sym2
Tactic: rw [← image_union, diag_union_offDiag, sym2_eq_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
rw : image (Function.uncurry Sym2.mk) (s.diag ∪ s.offDiag) = s.sym2
⊢ image (Function.uncurry Sym2.mk) s.diag ∪ image (Function.uncurry Sym2.mk) s.offDiag = s.sym2
have rw₁ : image (Function.uncurry Sym2.mk) (s ×ˢ s) = s.sym2
Tactic: rw [← image_union, diag_union_offDiag, sym2_eq_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
rw : image (Function.uncurry Sym2.mk) (s.diag ∪ s.offDiag) = s.sym2
rw₁ : image (Function.uncurry Sym2.mk) (s ×ˢ s) = s.sym2
⊢ image (Function.uncurry Sym2.mk) s.diag ∪ image (Function.uncurry Sym2.mk) s.offDiag = s.sym2
have rw₂ : image (Function.uncurry Sym2.mk) (s ×ˢ s) = image (Function.uncurry Sym2.mk) (s ×ˢ s)
Tactic: rw [← image_union, diag_union_offDiag, sym2_eq_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
m : Sym α 0
⊢ Membership.mem (γ := Finset (Sym α 0)) (s.sym 0) m ↔ ∀ a ∈ m, a ∈ s
have zero : m = ∅ → ∀ a ∈ m, a ∈ s
Tactic: refine mem_singleton.trans ⟨?_, fun _ ↦ Sym.eq_nil_of_card_zero _⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
m : Sym α n
⊢ m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
have succ : ∀ (n : ℕ) (ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s) {m : Sym α (n + 1)},
  Membership.mem (γ := Finset (Sym α (n + 1))) (s.sym (n + 1)) m ↔ ∀ a ∈ m, a ∈ s
Tactic: induction n with
  | zero =>
    refine mem_singleton.trans ⟨?_, fun _ ↦ Sym.eq_nil_of_card_zero _⟩
    rintro rfl
    exact fun a ha ↦ (Finset.notMem_empty _ ha).elim
  | succ n ih => ?_
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
⊢ Membership.mem (γ := Finset (Sym α (n + 1))) (s.sym (n + 1)) m ↔ ∀ a ∈ m, a ∈ s
have succ : (∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)) → ∀ a ∈ m, a ∈ s
Tactic: refine mem_sup.trans ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
succ : (∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)) → ∀ a ∈ m, a ∈ s
⊢ Membership.mem (γ := Finset (Sym α (n + 1))) (s.sym (n + 1)) m ↔ ∀ a ∈ m, a ∈ s
have succ₁ : ∀ (h : ∀ a ∈ m, a ∈ s), ∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)
Tactic: refine mem_sup.trans ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
a : α
ha : a ∈ s
he : m ∈ image (Sym.cons a) (s.sym n)
b : α
hb : b ∈ m
⊢ b ∈ s
have succ : ∀ (he : ∃ a_1 ∈ s.sym n, a ::ₛ a_1 = m) (b : α) (hb : b ∈ m), b ∈ s
Tactic: rw [mem_image] at he
Cleared hypotheses: he, b, hb
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
a : α
ha : a ∈ s
he : ∃ a_1 ∈ s.sym n, a ::ₛ a_1 = m
b : α
hb : b ∈ m
⊢ b ∈ s
have succ : ∀ (m : Sym α n) (he : m ∈ s.sym n) (hb : b ∈ a ::ₛ m), b ∈ s
Tactic: obtain ⟨m, he, rfl⟩ := he
Cleared hypotheses: m, he, hb
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (hypothesis)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
hb : b ∈ a ::ₛ m
⊢ b ∈ s
have hb₁ : b = a ∨ b ∈ m
Tactic: rw [Sym.mem_cons] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
hb : b = a ∨ b ∈ m
⊢ b ∈ s
have succ : ∀ (ha : b ∈ s), b ∈ s
Tactic: obtain rfl | hb := hb
Cleared hypotheses: a, ha, hb
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
hb : b = a ∨ b ∈ m
succ : ∀ (ha : b ∈ s), b ∈ s
⊢ b ∈ s
have succ₁ : ∀ (hb : b ∈ m), b ∈ s
Tactic: obtain rfl | hb := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n_1 n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
h : ∀ a ∈ m, a ∈ s
⊢ ∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)
have succ : ∀ (a : α) (m : Sym α n) (h : ∀ a_1 ∈ a ::ₛ m, a_1 ∈ s), ∃ i ∈ s, a ::ₛ m ∈ image (Sym.cons i) (s.sym n)
Tactic: obtain ⟨a, m, rfl⟩ := m.exists_eq_cons_of_succ
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
⊢ (map g s).sym n =
    map { toFun := Sym.map (⇑g : (a : α) → β), inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Sym α n) (Sym β n) }
      (s.sym n)
have h : ∀ (d : Sym β n),
  d ∈ (map g s).sym n ↔
    d ∈
      map { toFun := Sym.map (⇑g : (a : α) → β), inj' := sorry : Function.Embedding.{u_1 + 1, u_2 + 1} (Sym α n) (Sym β n) }
        (s.sym n)
Tactic: ext d
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
⊢ d ∈ (map g s).sym n ↔
    d ∈
      map { toFun := Sym.map (⇑g : (a : α) → β), inj' := ⋯ : Function.Embedding.{u_1 + 1, u_2 + 1} (Sym α n) (Sym β n) }
        (s.sym n)
have h : (∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a) ↔
  ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
Tactic: simp only [mem_sym_iff, mem_map, Function.Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
⊢ (∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a) ↔
    ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
have h : ∀ (hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a),
  ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
Tactic: refine ⟨fun hd ↦ ?_, fun ⟨b, hb, hd'⟩ d' hd ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
h :
  ∀ (hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a),
    ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
⊢ (∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a) ↔
    ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
have h₁ : (∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d) →
  ∀ (d' : β) (hd : d' ∈ d) (b : Sym α n) (hb : ∀ a ∈ b, a ∈ s) (hd' : Sym.map (⇑g : (a : α) → β) b = d),
    ∃ a ∈ s, (g : (a : α) → β) a = d'
Tactic: refine ⟨fun hd ↦ ?_, fun ⟨b, hb, hd'⟩ d' hd ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
⊢ ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
have h : ∀ (a : α), Membership.mem (γ := Sym α n) ((fun (p : Sym { x : β // x ∈ d } n) ↦ Sym.map g' p) d.attach) a → a ∈ s
Tactic: refine ⟨(fun p ↦ Sym.map g' p) d.attach, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
h : ∀ (a : α), Membership.mem (γ := Sym α n) ((fun (p : Sym { x : β // x ∈ d } n) ↦ Sym.map g' p) d.attach) a → a ∈ s
⊢ ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
have h₁ : Sym.map.{u_1, u_2} (α := α) (⇑g : (a : α) → β) ((fun (p : Sym { x : β // x ∈ d } n) ↦ Sym.map g' p) d.attach) = d
Tactic: refine ⟨(fun p ↦ Sym.map g' p) d.attach, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
⊢ ∀ (a : α), Membership.mem (γ := Sym α n) ((fun (p : Sym { x : β // x ∈ d } n) ↦ Sym.map g' p) d.attach) a → a ∈ s
have h : ∀ (a : α) (x : β) (x_1 : x ∈ d) (h : sorry.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x) = a), a ∈ s
Tactic: simp only [Sym.mem_map, Sym.mem_attach, true_and, Subtype.exists, forall_exists_index, g']
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
i : α
e : β
he : e ∈ d
hi : ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = e) = i
⊢ i ∈ s
have h : sorry.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = e) ∈ s
Tactic: rw [← hi]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
⊢ Sym.map.{u_1, u_2} (α := α) (⇑g : (a : α) → β) ((fun (p : Sym { x : β // x ∈ d } n) ↦ Sym.map g' p) d.attach) = d
have h : Sym.map
    (fun (x : { x : β // x ∈ d }) ↦
      (g : (a : α) → β) (sorry.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = (↑x : β))))
    d.attach =
  d
Tactic: simp only [Sym.map_map, Function.comp_apply, g']
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
⊢ Sym.map
      (fun (x : { x : β // x ∈ d }) ↦
        (g : (a : α) → β) (⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = (↑x : β))))
      d.attach =
    d
have h : ∀ (x : β) (hx : x ∈ d) (hx' : Subtype.mk (p := fun (x : β) ↦ x ∈ d) x hx ∈ d.attach),
  (g : (a : α) → β)
      (sorry.choose (p := fun (a : α) ↦
        a ∈ s ∧ (g : (a : α) → β) a = (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ d) x hx) : β))) =
    (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ d) x hx) : β)
Tactic: convert! Sym.attach_map_coe d with ⟨x, hx⟩ hx'
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
h : ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
d' : β
hd : d' ∈ d
b : Sym α n
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g : (a : α) → β) b = d
⊢ ∃ a ∈ s, (g : (a : α) → β) a = d'
have hd₁ : ∃ a ∈ b, (g : (a : α) → β) a = d'
Tactic: rw [← hd', Sym.mem_map] at hd
Cleared hypotheses: hd, hb, hd'
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
h : ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
d' : β
b : Sym α n
hd : ∃ a ∈ b, (g : (a : α) → β) a = d'
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g : (a : α) → β) b = d
⊢ ∃ a ∈ s, (g : (a : α) → β) a = d'
have h : ∀ (a : α) (ha : a ∈ b), ∃ a_1 ∈ s, Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) a_1 : β) ((g : (a : α) → β) a : β)
Tactic: obtain ⟨a, ha, rfl⟩ := hd
Cleared hypotheses: d', hd
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
h : s.sym n = ∅
⊢ s = ∅
have contrapose! : ∀ (h : s.Nonempty), (s.sym n).Nonempty
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
⊢ s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅
have zero : Eq (α := Finset (Sym α 0)) (s.sym 0) ∅ ↔ Ne (α := ℕ) 0 0 ∧ s = ∅
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
zero : Eq (α := Finset (Sym α 0)) (s.sym 0) ∅ ↔ Ne (α := ℕ) 0 0 ∧ s = ∅
⊢ s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅
have succ : ∀ (n : ℕ), Eq (α := Finset (Sym α (n + 1))) (s.sym (n + 1)) ∅ ↔ n + 1 ≠ 0 ∧ s = ∅
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
⊢ Eq (α := Finset (Sym α (n + 1))) (s.sym (n + 1)) ∅ ↔ n + 1 ≠ 0 ∧ s = ∅
have succ : n + 1 ≠ 0 ∧ s = ∅ → Eq (α := Finset (Sym α (n + 1))) (s.sym (n + 1)) ∅
Tactic: refine ⟨fun h ↦ ⟨Nat.succ_ne_zero _, eq_empty_of_sym_eq_empty h⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
⊢ (s.sym n).Nonempty ↔ n = 0 ∨ s.Nonempty
have contrapose! : s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
n : ℕ
⊢ (s ∩ t).sym n = s.sym n ∩ t.sym n
have h : ∀ (m : Sym α n), m ∈ (s ∩ t).sym n ↔ m ∈ s.sym n ∩ t.sym n
Tactic: ext m
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : DecidableEq α
n : ℕ
h : a ∉ s
m : ↥((insert a s).sym n)
⊢ Membership.mem (γ :=
    Finset
      (Sym α (n - (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ))))
    (s.sym (n - (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ)))
    ((Sym.filterNe a (↑m : Sym α n)).snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ))))
have h₁ : s = (insert a s).erase a
Tactic: convert! sym_filterNe_mem a m.2
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : DecidableEq α
n : ℕ
h : a ∉ s
m : ↥((insert a s).sym n)
⊢ s = (insert a s).erase a
have h₁ : s = s
Tactic: rw [erase_insert h]
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : DecidableEq α
n : ℕ
h : a ∉ s
x : (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))
i : Fin (n + 1)
m : Sym α (n - (↑i : ℕ))
hm : Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) m
⊢ Eq.{u_1 + 1} (α := (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
    ((fun (m : ↥((insert a s).sym n)) ↦
        (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
            ((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ))))
            (Subtype.mk (p :=
              fun
                (x :
                  Sym α
                    (n -
                      (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) :
                        ℕ))) ↦
              Membership.mem (γ :=
                Finset
                  (Sym α
                    (n -
                      (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) :
                        ℕ))))
                (s.sym
                  (n -
                    (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ)))
                x)
              ((Sym.filterNe a (↑m : Sym α n)).snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) ⋯) :
          (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))))
      ((fun (m : (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))) ↦
          Subtype.mk (p := fun (x : Sym α n) ↦ x ∈ (insert a s).sym n)
            (Sym.fill a (m.fst (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))))
              (↑(m.snd (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))) : Sym α (n - (↑m.fst : ℕ))))
            ⋯)
        (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) i
          (Subtype.mk (p := fun (x : Sym α (n - (↑i : ℕ))) ↦
            Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) x) m hm))))
    (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) i
      (Subtype.mk (p := fun (x : Sym α (n - (↑i : ℕ))) ↦
        Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) x) m hm))
have refine_1 : Fin (n + 1) → Type u_1
Tactic: refine Function.Injective.sigma_map (β₂ := ?_) (f₂ := ?_)
        (Function.injective_id) (fun i ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : DecidableEq α
n : ℕ
h : a ∉ s
x : (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))
i : Fin (n + 1)
m : Sym α (n - (↑i : ℕ))
hm : Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) m
refine_1 : Fin (n + 1) → Type u_1
⊢ Eq.{u_1 + 1} (α := (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
    ((fun (m : ↥((insert a s).sym n)) ↦
        (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
            ((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ))))
            (Subtype.mk (p :=
              fun
                (x :
                  Sym α
                    (n -
                      (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) :
                        ℕ))) ↦
              Membership.mem (γ :=
                Finset
                  (Sym α
                    (n -
                      (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) :
                        ℕ))))
                (s.sym
                  (n -
                    (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ)))
                x)
              ((Sym.filterNe a (↑m : Sym α n)).snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) ⋯) :
          (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))))
      ((fun (m : (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))) ↦
          Subtype.mk (p := fun (x : Sym α n) ↦ x ∈ (insert a s).sym n)
            (Sym.fill a (m.fst (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))))
              (↑(m.snd (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))) : Sym α (n - (↑m.fst : ℕ))))
            ⋯)
        (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) i
          (Subtype.mk (p := fun (x : Sym α (n - (↑i : ℕ))) ↦
            Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) x) m hm))))
    (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) i
      (Subtype.mk (p := fun (x : Sym α (n - (↑i : ℕ))) ↦
        Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) x) m hm))
have refine_2 : (a : Fin (n + 1)) → ↥(s.sym (n - (↑a : ℕ))) → Sym α (n - (↑(id a) : ℕ))
Tactic: refine Function.Injective.sigma_map (β₂ := ?_) (f₂ := ?_)
        (Function.injective_id) (fun i ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : DecidableEq α
n : ℕ
h : a ∉ s
x : (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))
i : Fin (n + 1)
m : Sym α (n - (↑i : ℕ))
hm : Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) m
refine_1 : Fin (n + 1) → Type u_1
refine_2 : (a : Fin (n + 1)) → ↥(s.sym (n - (↑a : ℕ))) → Sym α (n - (↑(id a) : ℕ))
⊢ Eq.{u_1 + 1} (α := (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
    ((fun (m : ↥((insert a s).sym n)) ↦
        (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
            ((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ))))
            (Subtype.mk (p :=
              fun
                (x :
                  Sym α
                    (n -
                      (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) :
                        ℕ))) ↦
              Membership.mem (γ :=
                Finset
                  (Sym α
                    (n -
                      (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) :
                        ℕ))))
                (s.sym
                  (n -
                    (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ)))
                x)
              ((Sym.filterNe a (↑m : Sym α n)).snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) ⋯) :
          (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))))
      ((fun (m : (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))) ↦
          Subtype.mk (p := fun (x : Sym α n) ↦ x ∈ (insert a s).sym n)
            (Sym.fill a (m.fst (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))))
              (↑(m.snd (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))) : Sym α (n - (↑m.fst : ℕ))))
            ⋯)
        (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) i
          (Subtype.mk (p := fun (x : Sym α (n - (↑i : ℕ))) ↦
            Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) x) m hm))))
    (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) i
      (Subtype.mk (p := fun (x : Sym α (n - (↑i : ℕ))) ↦
        Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) x) m hm))
have refine_3 : ∀ (i : Fin (n + 1)),
  Function.Injective (β := Sym α (n - (↑(id i) : ℕ))) fun (a : ↥(s.sym (n - (↑i : ℕ)))) ↦
    (↑a : Sym α (n - (↑(id i) : ℕ)))
Tactic: refine Function.Injective.sigma_map (β₂ := ?_) (f₂ := ?_)
        (Function.injective_id) (fun i ↦ ?_) ?_