awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
hy' : Sym2.Mem y' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y' (Quot.mk (Rel α) (x', y'))
hx₁ : True ∨ x = y ↔ x = x' ∨ x = y'
hy₁ : y = x ∨ True ↔ y = x' ∨ y = y'
hx'₁ : x' = x ∨ x' = y ↔ True ∨ x' = y'
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
have hy'₁ : y' = x ∨ y' = y ↔ y' = x' ∨ True
Tactic: simp only [mem_iff'] at hx hy hx' hy'
Cleared hypotheses: hx, hy, hx', hy'
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
e : Sym2 α
⊢ e = s((Quot.out (r := Rel α) e).1, (Quot.out (r := Rel α) e).2)
have rw : e = Quot.mk (Rel α) ((Quot.out (r := Rel α) e).1, (Quot.out (r := Rel α) e).2)
Tactic: rw [Sym2.mk, e.out_eq]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
e : Sym2 α
rw : e = Quot.mk (Rel α) ((Quot.out (r := Rel α) e).1, (Quot.out (r := Rel α) e).2)
⊢ e = s((Quot.out (r := Rel α) e).1, (Quot.out (r := Rel α) e).2)
have rw₁ : e = e
Tactic: rw [Sym2.mk, e.out_eq]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
e : Sym2 α
⊢ e = s((Quot.out (r := Rel α) e).2, (Quot.out (r := Rel α) e).1)
have rw : e = s((Quot.out (r := Rel α) e).1, (Quot.out (r := Rel α) e).2)
Tactic: rw [eq_swap, Sym2.mk, e.out_eq]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
e : Sym2 α
rw : e = s((Quot.out (r := Rel α) e).1, (Quot.out (r := Rel α) e).2)
⊢ e = s((Quot.out (r := Rel α) e).2, (Quot.out (r := Rel α) e).1)
have rw₁ : e = Quot.mk (Rel α) ((Quot.out (r := Rel α) e).1, (Quot.out (r := Rel α) e).2)
Tactic: rw [eq_swap, Sym2.mk, e.out_eq]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
e : Sym2 α
rw : e = s((Quot.out (r := Rel α) e).1, (Quot.out (r := Rel α) e).2)
rw₁ : e = Quot.mk (Rel α) ((Quot.out (r := Rel α) e).1, (Quot.out (r := Rel α) e).2)
⊢ e = s((Quot.out (r := Rel α) e).2, (Quot.out (r := Rel α) e).1)
have rw₂ : e = e
Tactic: rw [eq_swap, Sym2.mk, e.out_eq]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
x y : α
⊢ (↑s(x, y) : Set α) = {x, y}
have h : ∀ (z : α), z ∈ (↑s(x, y) : Set α) ↔ Membership.mem (γ := Set α) {x, y} z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
z : Sym2 α
⊢ (↑(map f z) : Set β) = f '' (↑z : Set α)
have h : ∀ (x y : α), (↑(map f s(x, y)) : Set β) = f '' (↑s(x, y) : Set α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z
have h₁ : z = s(a, Mem.other h)
Tactic: convert! mem_mk_right a <| Mem.other h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
⊢ z = s(a, Mem.other h)
have h₁ : z = z
Tactic: rw [other_spec h]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z ↔ z = s(x, y)
have mp : x ∈ z ∧ y ∈ z → z = s(x, y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
mp : x ∈ z ∧ y ∈ z → z = s(x, y)
⊢ x ∈ z ∧ y ∈ z ↔ z = s(x, y)
have mpr : z = s(x, y) → x ∈ z ∧ y ∈ z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z → z = s(x, y)
have mp : ∀ (x_1 y_1 : α), x ∈ s(x_1, y_1) ∧ y ∈ s(x_1, y_1) → s(x_1, y_1) = s(x, y)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
x y : α
hne : x ≠ y
x_1 y_1 : α
⊢ x ∈ s(x_1, y_1) ∧ y ∈ s(x_1, y_1) → s(x_1, y_1) = s(x, y)
have mp : (x = x_1 ∨ x = y_1) ∧ (y = x_1 ∨ y = y_1) → s(x_1, y_1) = s(x, y)
Tactic: rw [mem_iff, mem_iff]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
z : Sym2 α
⊢ b ∈ map f z ↔ ∃ a ∈ z, f a = b
have h : ∀ (x y : α), b ∈ map f s(x, y) ↔ ∃ a ∈ s(x, y), f a = b
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
⊢ map f s = map g s
have h₁ : ∀ (y : β), y ∈ map f s ↔ y ∈ map g s
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ y ∈ map f s ↔ y ∈ map g s
have h₁ : (∃ a ∈ s, f a = y) ↔ ∃ a ∈ s, g a = y
Tactic: simp only [mem_map]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ (∃ a ∈ s, f a = y) ↔ ∃ a ∈ s, g a = y
have h₁ : (∃ a ∈ s, f a = y) → ∃ a ∈ s, g a = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
h₁ : (∃ a ∈ s, f a = y) → ∃ a ∈ s, g a = y
⊢ (∃ a ∈ s, f a = y) ↔ ∃ a ∈ s, g a = y
have h₂ : (∃ a ∈ s, g a = y) → ∃ a ∈ s, f a = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (H : ∀ a ∈ s(p.1, p.2), P a) → Sym2 β :=
  fun (p : α × α) (H : ∀ a ∈ s(p.1, p.2), P a) ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq : Rel α p q
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
⊢ Eq.ndrec (motive := fun (x : Sym2 α) ↦ (∀ a ∈ x, P a) → Sym2 β) (g p) ⋯ Hq = g q Hq
have rw : ∀ (hpq_1 : p = q ∨ p = q.swap) (Hq : ∀ a ∈ Quot.mk (Rel α) q, P a),
  Eq.ndrec (motive := fun (x : Sym2 α) ↦ (∀ a ∈ x, P a) → Sym2 β) (g p) sorry Hq = g q Hq
Tactic: rw [rel_iff'] at hpq
Cleared hypotheses: Hq
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (H : ∀ a ∈ s(p.1, p.2), P a) → Sym2 β :=
  fun (p : α × α) (H : ∀ a ∈ s(p.1, p.2), P a) ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq_1 : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
⊢ Eq.ndrec (motive := fun (x : Sym2 α) ↦ (∀ a ∈ x, P a) → Sym2 β) (g p) ⋯ Hq = g q Hq
have Hp : ∀ a ∈ s(p.1, p.2), P a
Tactic: have Hp : ∀ a ∈ s(p.1, p.2), P a := fun a hmem =>
      Hq a (Sym2.mk_eq_mk_iff.2 hpq ▸ hmem : a ∈ s(q.1, q.2))
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (H : ∀ a ∈ s(p.1, p.2), P a) → Sym2 β :=
  fun (p : α × α) (H : ∀ a ∈ s(p.1, p.2), P a) ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq_1 : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
⊢ Eq.ndrec (motive := fun (x : Sym2 α) ↦ (∀ a ∈ x, P a) → Sym2 β) (g p) ⋯ Hq = g q Hq
have h : ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
  Eq.ndrec (motive := fun (s : Sym2 α) ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
Tactic: have h : ∀ {s₂ e H}, Eq.ndrec (motive := fun s => (∀ a ∈ s, P a) → Sym2 β) (g p) (b := s₂) e H =
      g p Hp := by
      rintro s₂ rfl _
      rfl
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (H : ∀ a ∈ s(p.1, p.2), P a) → Sym2 β :=
  fun (p : α × α) (H : ∀ a ∈ s(p.1, p.2), P a) ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq_1 : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun (s : Sym2 α) ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
⊢ Eq.ndrec (motive := fun (x : Sym2 α) ↦ (∀ a ∈ x, P a) → Sym2 β) (g p) ⋯ Hq = g q Hq
have refine : Rel β (f p.1 sorry, f p.2 sorry) (f q.1 sorry, f q.2 sorry)
Tactic: refine h.trans (Quot.sound ?_)
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (H : ∀ a ∈ s(p.1, p.2), P a) → Sym2 β :=
  fun (p : α × α) (H : ∀ a ∈ s(p.1, p.2), P a) ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq_1 : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun (s : Sym2 α) ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
⊢ Rel β (f p.1 ⋯, f p.2 ⋯) (f q.1 ⋯, f q.2 ⋯)
have rw : f p.1 sorry = f q.1 sorry ∧ f p.2 sorry = f q.2 sorry ∨ (f p.1 sorry, f p.2 sorry) = (f q.2 sorry, f q.1 sorry)
Tactic: rw [rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (H : ∀ a ∈ s(p.1, p.2), P a) → Sym2 β :=
  fun (p : α × α) (H : ∀ a ∈ s(p.1, p.2), P a) ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq_1 : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun (s : Sym2 α) ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
⊢ f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯ ∨ (f p.1 ⋯, f p.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)
have f₁ : p = q → f p.1 sorry = f q.1 sorry ∧ f p.2 sorry = f q.2 sorry
Tactic: apply hpq.imp
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (H : ∀ a ∈ s(p.1, p.2), P a) → Sym2 β :=
  fun (p : α × α) (H : ∀ a ∈ s(p.1, p.2), P a) ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq_1 : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun (s : Sym2 α) ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
f₁ : p = q → f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯
⊢ f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯ ∨ (f p.1 ⋯, f p.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)
have g₁ : p = q.swap → (f p.1 sorry, f p.2 sorry) = (f q.2 sorry, f q.1 sorry)
Tactic: apply hpq.imp
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
z : Sym2 α
h : ∀ a ∈ z, P a
b : β
⊢ b ∈ pmap (P := P) f z h ↔ ∃ (a : α) (ha : a ∈ z), b = f a ⋯
have mk : ∀ (x y : α) (h : ∀ a ∈ Quot.mk (Rel α) (x, y), P a),
  b ∈ pmap (P := P) f (Quot.mk (Rel α) (x, y)) h ↔ ∃ (a : α) (ha : a ∈ Quot.mk (Rel α) (x, y)), b = f a sorry
Tactic: obtain ⟨x, y⟩ := z
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
z : Sym2 α
b : β
x y : α
h : ∀ a ∈ Quot.mk (Rel α) (x, y), P a
⊢ b ∈ pmap (P := P) f (Quot.mk (Rel α) (x, y)) h ↔ ∃ (a : α) (ha : a ∈ Quot.mk (Rel α) (x, y)), b = f a ⋯
have mk : b ∈ s(f x sorry, f y sorry) ↔ ∃ (a : α) (ha : a ∈ Quot.mk (Rel α) (x, y)), b = f a sorry
Tactic: rw [pmap_pair f x y h]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
P : α → Prop
f : α → β
z : Sym2 α
h : ∀ a ∈ z, P a
⊢ pmap (P := P) (fun (a : α) (x : P a) ↦ f a) z h = map f z
have h₁ : ∀ (x y : α) (h : ∀ a ∈ s(x, y), P a), pmap (P := P) (fun (a : α) (x : P a) ↦ f a) s(x, y) h = map f s(x, y)
Tactic: cases z
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Q : β → Prop
f : α → β
g : (b : β) → Q b → γ
z : Sym2 α
h : ∀ b ∈ map f z, Q b
⊢ pmap (P := Q) g (map f z) h = pmap (P := Membership.mem z) (fun (a : α) (ha : a ∈ z) ↦ g (f a) ⋯) z ⋯
have h₁ : ∀ (x y : α) (h : ∀ b ∈ map f s(x, y), Q b),
  pmap (P := Q) g (map f s(x, y)) h =
    pmap (P := Membership.mem s(x, y)) (fun (a : α) (ha : a ∈ s(x, y)) ↦ g (f a) sorry) s(x, y) sorry
Tactic: cases z
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : β → γ
z : Sym2 α
h : ∀ a ∈ z, P a
h' : ∀ b ∈ pmap (P := P) f z h, Q b
⊢ map g (pmap (P := P) f z h) = pmap (P := Membership.mem z) (fun (a : α) (ha : a ∈ z) ↦ g (f a ⋯)) z ⋯
have h₁ : ∀ (x y : α) (h : ∀ a ∈ s(x, y), P a) (h' : ∀ b ∈ pmap (P := P) f s(x, y) h, Q b),
  map g (pmap (P := P) f s(x, y) h) =
    pmap (P := Membership.mem s(x, y)) (fun (a : α) (ha : a ∈ s(x, y)) ↦ g (f a sorry)) s(x, y) sorry
Tactic: cases z
Cleared hypotheses: z, h, h'
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : (b : β) → Q b → γ
z : Sym2 α
h : ∀ a ∈ z, P a
h' : ∀ b ∈ pmap (P := P) f z h, Q b
⊢ pmap (P := Q) g (pmap (P := P) f z h) h' = pmap (P := Membership.mem z) (fun (a : α) (ha : a ∈ z) ↦ g (f a ⋯) ⋯) z ⋯
have h₁ : ∀ (x y : α) (h : ∀ a ∈ s(x, y), P a) (h' : ∀ b ∈ pmap (P := P) f s(x, y) h, Q b),
  pmap (P := Q) g (pmap (P := P) f s(x, y) h) h' =
    pmap (P := Membership.mem s(x, y)) (fun (a : α) (ha : a ∈ s(x, y)) ↦ g (f a sorry) sorry) s(x, y) sorry
Tactic: cases z
Cleared hypotheses: z, h, h'
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
P : α → Prop
s : Sym2 α
h : ∀ a ∈ s, P a
⊢ map (Subtype.val (p := P)) (pmap (P := P) (Subtype.mk (p := P)) s h) = s
have h₁ : ∀ (x y : α) (h : ∀ a ∈ s(x, y), P a),
  map (Subtype.val (p := P)) (pmap (P := P) (Subtype.mk (p := P)) s(x, y) h) = s(x, y)
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
s : Sym2 α
P : α → Prop
h : ∀ a ∈ s, P a
⊢ map (Subtype.val (p := fun (a : α) ↦ P a)) (s.attachWith (P := P) h) = s
have h₁ : ∀ (x y : α) (h : ∀ a ∈ s(x, y), P a),
  map (Subtype.val (p := fun (a : α) ↦ P a)) (s(x, y).attachWith (P := P) h) = s(x, y)
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
x y : α
h : diag x = diag y
⊢ x = y
have refl : ∀ (h : diag x = diag x), x = x
Tactic: cases Sym2.exact h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) (Set.range diag) diagSet
have h : ∀ (x : Sym2 α) (a b : α),
  Membership.mem (γ := Set (Sym2 α)) (Set.range diag) (Quot.mk (Rel α) (a, b)) ↔
    Membership.mem (γ := Set (Sym2 α)) diagSet (Quot.mk (Rel α) (a, b))
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : Subsingleton α
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) diagSet Set.univ
have h : ∀ (x : Sym2 α), Membership.mem (γ := Set (Sym2 α)) diagSet x ↔ Membership.mem (γ := Set (Sym2 α)) Set.univ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a : α
z : Sym2 α
hd : ¬z.IsDiag
h : a ∈ z
⊢ Mem.other h ≠ a
have contrapose : ∀ (hd : Mem.other h = a), z.IsDiag
Tactic: contrapose hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
⊢ z.IsDiag
have h' : s(a, Mem.other h) = z
Tactic: have h' := Sym2.other_spec h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, Mem.other h) = z
⊢ z.IsDiag
have h'₁ : s(a, a) = z
Tactic: rw [hd] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, a) = z
⊢ z.IsDiag
have rw : s(a, a).IsDiag
Tactic: rw [← h']
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
⊢ fromRel (r := r) sym = ∅ ↔ r = ⊥
have refine : ∀ (h : fromRel (r := r) sym = ∅), r = ⊥
Tactic: refine ⟨fun h ↦ ?_, (· ▸ fromRel_bot)⟩
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
h : fromRel (r := r) sym = ∅
⊢ r = ⊥
have h₁ : ∀ (x y : α), r x y ↔ ⊥ x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
⊢ fromRel (r := r) sym = Set.univ ↔ r = ⊤
have refine : ∀ (h : fromRel (r := r) sym = Set.univ), r = ⊤
Tactic: refine ⟨fun h ↦ ?_, (· ▸ fromRel_top)⟩
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
h : fromRel (r := r) sym = Set.univ
⊢ r = ⊤
have h₁ : ∀ (x y : α), r x y ↔ ⊤ x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) (fromRel (r := Ne) ⋯) {z : Sym2 α | ¬z.IsDiag}
have h : ∀ (z : Sym2 α),
  Membership.mem (γ := Set (Sym2 α)) (fromRel (r := Ne) sorry) z ↔
    Membership.mem (γ := Set (Sym2 α)) {z : Sym2 α | ¬z.IsDiag} z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) diagSet (fromRel (r := Eq) ⋯)
have h : ∀ (x : Sym2 α) (a b : α),
  Membership.mem (γ := Set (Sym2 α)) diagSet (Quot.mk (Rel α) (a, b)) ↔
    Membership.mem (γ := Set (Sym2 α)) (fromRel (r := Eq) sorry) (Quot.mk (Rel α) (a, b))
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) diagSetᶜ (fromRel (r := Ne) ⋯)
have h : ∀ (x : Sym2 α) (a b : α),
  Membership.mem (γ := Set (Sym2 α)) diagSetᶜ (Quot.mk (Rel α) (a, b)) ↔
    Membership.mem (γ := Set (Sym2 α)) (fromRel (r := Ne) sorry) (Quot.mk (Rel α) (a, b))
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
h : ∀ (a : α), ¬r a a
⊢ ∀ {z : Sym2 α}, z ∈ fromRel (r := r) sym → ¬z.IsDiag
have h₁ : ∀ (x y : α), s(x, y) ∈ fromRel (r := r) sym → ¬s(x, y).IsDiag
Tactic: apply Sym2.ind
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
hr : Symmetric r
f : α → β
⊢ fromRel (r := Relation.Map r f f) ⋯ = map f '' fromRel (r := r) hr
have h : ∀ (x : Sym2 β) (a b : β),
  Quot.mk (Rel β) (a, b) ∈ fromRel (r := Relation.Map r f f) sorry ↔ Quot.mk (Rel β) (a, b) ∈ map f '' fromRel (r := r) hr
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
hr : Symmetric r
f : α → β
x : Sym2 β
a b : β
⊢ Quot.mk (Rel β) (a, b) ∈ fromRel (r := Relation.Map r f f) ⋯ ↔ Quot.mk (Rel β) (a, b) ∈ map f '' fromRel (r := r) hr
have h : ∀ (x x_1 : α), r x x_1 → f x = b → f x_1 = a → ∃ (a_4 : α) (b_1 : α), r a_4 b_1 ∧ f a_4 = a ∧ f b_1 = b
Tactic: simp only [fromRel_prop, Relation.Map, Set.mem_image, Sym2.exists, map_mk, Sym2.eq,
    rel_iff', Prod.mk.injEq, Prod.swap_prod_mk, and_or_left, exists_or, iff_self_or,
    forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
r₁ r₂ : α → α → Prop
sym₁ : Symmetric r₁
sym₂ : Symmetric r₂
⊢ fromRel (r := r₁) sym₁ = fromRel (r := r₂) sym₂ ↔ r₁ = r₂
have rw : fromRel (r := r₁) sym₁ = fromRel (r := r₂) sym₂ ↔
  Eq (α := Set (Sym2 α))
    ((fromRelOrderIso α : (a : { r : α → α → Prop // Symmetric r }) → Set (Sym2 α))
        (Subtype.mk (p := Symmetric) r₁ sym₁) :
      Set (Sym2 α))
    ((fromRelOrderIso α : (a : { r : α → α → Prop // Symmetric r }) → Set (Sym2 α))
        (Subtype.mk (p := Symmetric) r₂ sym₂) :
      Set (Sym2 α))
Tactic: rw [← Subtype.mk.injEq r₁ sym₁ r₂ sym₂, ← fromRelOrderIso α |>.eq_iff_eq]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
z_1 : Sym2 α_1
f : α_1 → β
α : Type u_4
z : Sym2 α
⊢ Multiset α
have refine : { f : α → α → Multiset α // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
Tactic: refine Sym2.lift ?_ z
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
z_1 : Sym2 α_1
f : α_1 → β
α : Type u_4
z : Sym2 α
⊢ { f : α → α → Multiset α // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
have property : ∀ (a₁ a₂ : α),
  Eq.{u_4 + 1} (α := Multiset α) ((fun (x1 x2 : α) ↦ (↑[x1, x2] : Multiset α)) a₁ a₂)
    ((fun (x1 x2 : α) ↦ (↑[x1, x2] : Multiset α)) a₂ a₁)
Tactic: use (Multiset.ofList [·, ·])
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_4
z : Sym2 α
⊢ z.toMultiset.card = 2
have h : ∀ (x y : α), s(x, y).toMultiset.card = 2
Tactic: induction z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_4
x : α
z : Sym2 α
⊢ x ∈ z.toMultiset ↔ x ∈ z
have h : ∀ (x_1 y : α), x ∈ s(x_1, y).toMultiset ↔ x ∈ s(x_1, y)
Tactic: induction z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
z : Sym2 α
⊢ x ∈ z.toFinset ↔ x ∈ z
have rw : x ∈ z.toFinset ↔ x ∈ z.toMultiset
Tactic: rw [← Sym2.mem_toMultiset, Sym2.toFinset, Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
z : Sym2 α
rw : x ∈ z.toFinset ↔ x ∈ z.toMultiset
⊢ x ∈ z.toFinset ↔ x ∈ z
have rw₁ : x ∈ z.toMultiset.toFinset ↔ x ∈ z.toMultiset
Tactic: rw [← Sym2.mem_toMultiset, Sym2.toFinset, Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
z : Sym2 α
rw : x ∈ z.toFinset ↔ x ∈ z.toMultiset
rw₁ : x ∈ z.toMultiset.toFinset ↔ x ∈ z.toMultiset
⊢ x ∈ z.toFinset ↔ x ∈ z
have rw₂ : x ∈ z.toMultiset ↔ x ∈ z.toMultiset
Tactic: rw [← Sym2.mem_toMultiset, Sym2.toFinset, Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
⊢ s(x, y).toFinset = {x, y}
have h : ∀ (a : α), a ∈ s(x, y).toFinset ↔ Membership.mem (γ := Finset α) {x, y} a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
z : Sym2 α
h : z.IsDiag
⊢ #z.toFinset = 1
have h₁ : ∀ (x y : α) (h : s(x, y).IsDiag), #s(x, y).toFinset = 1
Tactic: induction z
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
h : s(x, y).IsDiag
⊢ #s(x, y).toFinset = 1
have h₁ : x = y
Tactic: rw [Sym2.mk_isDiag_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
z : Sym2 α
h : ¬z.IsDiag
⊢ #z.toFinset = 2
have h₁ : ∀ (x y : α) (h : ¬s(x, y).IsDiag), #s(x, y).toFinset = 2
Tactic: induction z
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
h : ¬s(x, y).IsDiag
⊢ #s(x, y).toFinset = 2
have h₁ : ¬x = y
Tactic: rw [Sym2.mk_isDiag_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
z : Sym2 α
⊢ #z.toFinset = if z.IsDiag then 1 else 2
have pos : ∀ (h : z.IsDiag), #z.toFinset = if z.IsDiag then 1 else 2
Tactic: by_cases h : z.IsDiag
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
inst : DecidableEq α
z : Sym2 α
pos : ∀ (h : z.IsDiag), #z.toFinset = if z.IsDiag then 1 else 2
⊢ #z.toFinset = if z.IsDiag then 1 else 2
have neg : ∀ (h : ¬z.IsDiag), #z.toFinset = if z.IsDiag then 1 else 2
Tactic: by_cases h : z.IsDiag
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
⊢ [a₁, b₁].Perm [a₂, b₂] → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
have simp : a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
Tactic: simp only [← Multiset.coe_eq_coe, ← Multiset.cons_coe, Multiset.coe_nil, Multiset.cons_zero,
        Multiset.cons_eq_cons, Multiset.singleton_inj, ne_eq, Multiset.singleton_eq_cons_iff,
        exists_eq_right_right, and_true]
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2 (goal)
Goal:
α : Type u_1
a₁ b₁ a₂ b₂ : α
⊢ a₁ = a₂ ∧ b₁ = b₂ ∨ ¬a₁ = a₂ ∧ b₁ = a₂ ∧ b₂ = a₁ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
have inl : a₁ = a₂ → b₁ = b₂ → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂
Tactic: tauto