awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sym.Sym2
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
refine : Rel β (f p.1 ⋯, f p.2 ⋯) (f q.1 ⋯, f q.2 ⋯)
⊢ Eq.ndrec (motive := fun (x : Sym2 α) ↦ (∀ a ∈ x, P a) → Sym2 β) (g p) ⋯ Hq = g q Hq

Tactic:
refine h.trans (Quot.sound ?_)

Premises used: Quot.sound, Eq.trans
-- Module: Mathlib.Data.Sym.Sym2
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
rw : f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯ ∨ (f p.1 ⋯, f p.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)
⊢ Rel β (f p.1 ⋯, f p.2 ⋯) (f q.1 ⋯, f q.2 ⋯)

Tactic:
rw [rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]

Premises used: Prod.swap_prod_mk, Sym2.rel_iff', Prod.mk.injEq
-- Module: Mathlib.Data.Sym.Sym2
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 ⋯
g₁ : p = q.swap → (f p.1 ⋯, f p.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)
⊢ f p.1 ⋯ = f q.1 ⋯ ∧ f p.2 ⋯ = f q.2 ⋯ ∨ (f p.1 ⋯, f p.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)

Tactic:
apply hpq.imp

Premises used: Or.imp
-- Module: Mathlib.Data.Sym.Sym2
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 : α × α
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
hpq_1 : Rel α p p
hpq : p = p ∨ p = p.swap
Hq : ∀ a ∈ Quot.mk (Rel α) p, P a
⊢ f p.1 ⋯ = f p.1 ⋯ ∧ f p.2 ⋯ = f p.2 ⋯

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
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 ⋯)
q : α × α
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
hpq_1 : Rel α q.swap q
hpq : q.swap = q ∨ q.swap = q.swap
Hp : ∀ a ∈ s(q.swap.1, q.swap.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(q.swap.1, q.swap.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun (s : Sym2 α) ↦ (∀ a ∈ s, P a) → Sym2 β) (g q.swap) e H = g q.swap Hp
⊢ (f q.swap.1 ⋯, f q.swap.2 ⋯) = (f q.2 ⋯, f q.1 ⋯)

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
P : α → Prop
a b : α
⊢ (∀ x ∈ s(a, b), P x) ↔ P a ∧ P b

Tactic:
simp only [mem_iff, forall_eq_or_imp, forall_eq]

Premises used: forall_eq, forall_eq_or_imp, Sym2.mem_iff
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
a b : α
h : P a
h' : P b
⊢ s(f a h, f b h') = pmap (P := P) f s(a, b) ⋯

Tactic:
rfl

Premises used: Sym2.pmap, rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
a b : α
h : ∀ x ∈ s(a, b), P x
⊢ pmap (P := P) f s(a, b) h = s(f a ⋯, f b ⋯)

Tactic:
rfl

Premises used: Sym2.pmap, rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
z : Sym2 α
h : ∀ a ∈ z, P a
b : β
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 ⋯
⊢ b ∈ pmap (P := P) f z h ↔ ∃ (a : α) (ha : a ∈ z), b = f a ⋯

Tactic:
obtain ⟨x, y⟩ := z
-- Module: Mathlib.Data.Sym.Sym2
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
mk : b ∈ s(f x ⋯, f y ⋯) ↔ ∃ (a : α) (ha : a ∈ Quot.mk (Rel α) (x, y)), b = f a ⋯
⊢ b ∈ pmap (P := P) f (Quot.mk (Rel α) (x, y)) h ↔ ∃ (a : α) (ha : a ∈ Quot.mk (Rel α) (x, y)), b = f a ⋯

Tactic:
rw [pmap_pair f x y h]

Premises used: Sym2.pmap_pair
-- Module: Mathlib.Data.Sym.Sym2
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 ∈ s(f x ⋯, f y ⋯) ↔ ∃ (a : α) (ha : a ∈ Quot.mk (Rel α) (x, y)), b = f a ⋯

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
P : α → Prop
f : α → β
z : Sym2 α
h : ∀ a ∈ z, P a
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)
⊢ pmap (P := P) (fun (a : α) (x : P a) ↦ f a) z h = map f z

Tactic:
cases z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
P : α → Prop
f : α → β
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:
rfl
-- Module: Mathlib.Data.Sym.Sym2
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
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) ⋯) s(x, y) ⋯
⊢ pmap (P := Q) g (map f z) h = pmap (P := Membership.mem z) (fun (a : α) (ha : a ∈ z) ↦ g (f a) ⋯) z ⋯

Tactic:
cases z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Q : β → Prop
f : α → β
g : (b : β) → Q b → γ
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) ⋯) s(x, y) ⋯

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Sym2
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
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 ⋯)) s(x, y) ⋯
⊢ map g (pmap (P := P) f z h) = pmap (P := Membership.mem z) (fun (a : α) (ha : a ∈ z) ↦ g (f a ⋯)) z ⋯

Tactic:
cases z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : β → γ
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 ⋯)) s(x, y) ⋯

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Sym2
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
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 ⋯) ⋯) s(x, y) ⋯
⊢ 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 ⋯

Tactic:
cases z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : (b : β) → Q b → γ
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 ⋯) ⋯) s(x, y) ⋯

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
P : α → Prop
s : Sym2 α
h : ∀ a ∈ s, P a
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)
⊢ map (Subtype.val (p := P)) (pmap (P := P) (Subtype.mk (p := P)) s h) = s

Tactic:
cases s
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
P : α → Prop
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:
rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
s : Sym2 α
P : α → Prop
h : ∀ a ∈ s, P a
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)
⊢ map (Subtype.val (p := fun (a : α) ↦ P a)) (s.attachWith (P := P) h) = s

Tactic:
cases s
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
P : α → Prop
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:
rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y : α
h : diag x = diag y
refl swap : ∀ (h : diag x = diag x), x = x
⊢ x = y

Tactic:
cases Sym2.exact h

Premises used: Sym2.exact
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x : α
h : diag x = diag x
⊢ x = x

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x y : α
⊢ s(x, y).IsDiag ↔ x = y

Tactic:
Iff.rfl

Premises used: Iff.rfl, Sym2.IsDiag
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
z : Sym2 α
f : α → β
⊢ z.IsDiag → (map f z).IsDiag

Tactic:
Sym2.ind (fun _ _ ↦ congr_arg f) z

Premises used: Sym2.ind
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
z : Sym2 α
f : α → β
hf : Injective f
⊢ (map f z).IsDiag ↔ z.IsDiag

Tactic:
Sym2.ind (fun _ _ ↦ hf.eq_iff) z

Premises used: Sym2.ind
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
⊢ (diag a).IsDiag

Tactic:
Eq.refl a

Premises used: Eq.refl, Sym2.IsDiag
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : Subsingleton α
z : Sym2 α
⊢ z.IsDiag

Tactic:
z.ind Subsingleton.elim

Premises used: Sym2.ind
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
z : Sym2 α
⊢ Membership.mem (γ := Set (Sym2 α)) diagSet z ↔ z.IsDiag

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Sym2.diagSet, Sym2.IsDiag
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
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))
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) (Set.range diag) diagSet

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
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:
simp [diag, eq_comm]

Premises used: eq_comm, Sym2.diag
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) diagSet {z : Sym2 α | z.IsDiag}

Tactic:
rfl

Premises used: Sym2.diagSet, rfl
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) diagSetᶜ {z : Sym2 α | ¬z.IsDiag}

Tactic:
congrArg _ diagSet_eq_setOf_isDiag

Premises used: congrArg, Set.Mem, setOf, Sym2.diagSet_eq_setOf_isDiag, Sym2.IsDiag
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : Subsingleton α
h : ∀ (x : Sym2 α), Membership.mem (γ := Set (Sym2 α)) diagSet x ↔ Membership.mem (γ := Set (Sym2 α)) Set.univ x
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) diagSet Set.univ

Tactic:
ext
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
inst : Subsingleton α
x : Sym2 α
⊢ Membership.mem (γ := Set (Sym2 α)) diagSet x ↔ Membership.mem (γ := Set (Sym2 α)) Set.univ x

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
z : Sym2 α
hd : ¬z.IsDiag
h : a ∈ z
contrapose : ∀ (hd : Mem.other h = a), z.IsDiag
⊢ Mem.other h ≠ a

Tactic:
contrapose hd
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
⊢ s(a, Mem.other h) = z

Tactic:
have h' := Sym2.other_spec h
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, Mem.other h) = z
⊢ s(a, a) = z

Tactic:
rw [hd] at h'
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, a) = z
rw : s(a, a).IsDiag
⊢ z.IsDiag

Tactic:
rw [← h']
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, a) = z
⊢ s(a, a).IsDiag

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
a b : α
⊢ s(a, b) ∈ fromRel (r := r) sym ↔ r a b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Sym2.fromRel
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r₁ r₂ : α → α → Prop
sym₁ : Symmetric r₁
sym₂ : Symmetric r₂
⊢ fromRel (r := r₁) sym₁ ⊆ fromRel (r := r₂) sym₂ ↔ r₁ ≤ r₂

Tactic:
⟨fun hle a b ↦ @hle s(a, b), fun hle ↦ Sym2.ind hle⟩

Premises used: Sym2.ind, Iff.intro
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
⊢ ∀ (x y : α), s(x, y) ∉ fromRel (r := ⊥) ⋯

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
⊢ fromRel (r := r) sym = ∅ ↔ r = ⊥

Tactic:
⟨fun h ↦ ?_, (· ▸ fromRel_bot)⟩

Premises used: Sym2.fromRel_bot, Iff.intro, Eq.symm
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
refine : ∀ (h : fromRel (r := r) sym = ∅), r = ⊥
⊢ fromRel (r := r) sym = ∅ ↔ r = ⊥

Tactic:
refine ⟨fun h ↦ ?_, (· ▸ fromRel_bot)⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
h : fromRel (r := r) sym = ∅
h₁ : ∀ (x y : α), r x y ↔ ⊥ x y
⊢ r = ⊥

Tactic:
ext x y
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
h : fromRel (r := r) sym = ∅
x y : α
⊢ r x y ↔ ⊥ x y

Tactic:
simpa [h] using fromRel_prop (sym := sym)

Premises used: Sym2.fromRel_prop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
⊢ ∀ (x y : α), Membership.mem (γ := Set (Sym2 α)) (fromRel (r := ⊤) ⋯) s(x, y)

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
⊢ fromRel (r := r) sym = Set.univ ↔ r = ⊤

Tactic:
⟨fun h ↦ ?_, (· ▸ fromRel_top)⟩

Premises used: Sym2.fromRel_top, Iff.intro, Eq.symm
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
refine : ∀ (h : fromRel (r := r) sym = Set.univ), r = ⊤
⊢ fromRel (r := r) sym = Set.univ ↔ r = ⊤

Tactic:
refine ⟨fun h ↦ ?_, (· ▸ fromRel_top)⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
h : fromRel (r := r) sym = Set.univ
h₁ : ∀ (x y : α), r x y ↔ ⊤ x y
⊢ r = ⊤

Tactic:
ext x y
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
h : fromRel (r := r) sym = Set.univ
x y : α
⊢ r x y ↔ ⊤ x y

Tactic:
simpa [h] using fromRel_prop (sym := sym)

Premises used: Sym2.fromRel_prop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
h :
  ∀ (z : Sym2 α),
    Membership.mem (γ := Set (Sym2 α)) (fromRel (r := Ne) ⋯) z ↔
      Membership.mem (γ := Set (Sym2 α)) {z : Sym2 α | ¬z.IsDiag} z
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) (fromRel (r := Ne) ⋯) {z : Sym2 α | ¬z.IsDiag}

Tactic:
ext z
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
z : Sym2 α
⊢ ∀ (x y : α),
    Membership.mem (γ := Set (Sym2 α)) (fromRel (r := Ne) ⋯) s(x, y) ↔
      Membership.mem (γ := Set (Sym2 α)) {z : Sym2 α | ¬z.IsDiag} s(x, y)

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
z : Sym2 α
⊢ Membership.mem (γ := Set (Sym2 α)) (fromRel (r := Ne) ⋯) z ↔
    Membership.mem (γ := Set (Sym2 α)) {z : Sym2 α | ¬z.IsDiag} z

Tactic:
exact z.ind (by simp)
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
h :
  ∀ (x : Sym2 α) (a b : α),
    Membership.mem (γ := Set (Sym2 α)) diagSet (Quot.mk (Rel α) (a, b)) ↔
      Membership.mem (γ := Set (Sym2 α)) (fromRel (r := Eq) ⋯) (Quot.mk (Rel α) (a, b))
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) diagSet (fromRel (r := Eq) ⋯)

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x : Sym2 α
a b : α
⊢ Membership.mem (γ := Set (Sym2 α)) diagSet (Quot.mk (Rel α) (a, b)) ↔
    Membership.mem (γ := Set (Sym2 α)) (fromRel (r := Eq) ⋯) (Quot.mk (Rel α) (a, b))

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
h :
  ∀ (x : Sym2 α) (a b : α),
    Membership.mem (γ := Set (Sym2 α)) diagSetᶜ (Quot.mk (Rel α) (a, b)) ↔
      Membership.mem (γ := Set (Sym2 α)) (fromRel (r := Ne) ⋯) (Quot.mk (Rel α) (a, b))
⊢ Eq.{u_1 + 1} (α := Set (Sym2 α)) diagSetᶜ (fromRel (r := Ne) ⋯)

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
x : Sym2 α
a b : α
⊢ Membership.mem (γ := Set (Sym2 α)) diagSetᶜ (Quot.mk (Rel α) (a, b)) ↔
    Membership.mem (γ := Set (Sym2 α)) (fromRel (r := Ne) ⋯) (Quot.mk (Rel α) (a, b))

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
hr : Symmetric r
⊢ diagSet ⊆ fromRel (r := r) hr ↔ Std.Refl r

Tactic:
simp [Set.subset_def, Sym2.forall, refl_def]

Premises used: Set.subset_def, refl_def, Sym2.forall
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
hr : Symmetric r
⊢ Disjoint diagSet (fromRel (r := r) hr) ↔ Std.Irrefl r

Tactic:
simp [Set.disjoint_left, Sym2.forall, irrefl_def]

Premises used: Set.disjoint_left, Sym2.forall, irrefl_def
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
hr : Symmetric r
⊢ fromRel (r := r) hr ⊆ diagSetᶜ ↔ Std.Irrefl r

Tactic:
simp [Set.subset_compl_iff_disjoint_left]

Premises used: Set.subset_compl_iff_disjoint_left
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
⊢ Std.Refl r ↔ diagSet ⊆ fromRel (r := r) sym

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
⊢ Std.Irrefl r ↔ fromRel (r := r) sym ⊆ diagSetᶜ

Tactic:
simp
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
h : ∀ (a : α), ¬r a a
h₁ : ∀ (x y : α), s(x, y) ∈ fromRel (r := r) sym → ¬s(x, y).IsDiag
⊢ ∀ {z : Sym2 α}, z ∈ fromRel (r := r) sym → ¬z.IsDiag

Tactic:
apply Sym2.ind
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
h : ∀ (a : α), ¬r a a
⊢ ∀ (x y : α), s(x, y) ∈ fromRel (r := r) sym → ¬s(x, y).IsDiag

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
irrefl : Std.Irrefl r
a : α
z : Sym2 α
hz : z ∈ fromRel (r := r) sym
h : a ∈ z
⊢ Mem.other h ≠ a

Tactic:
other_ne (fromRel_irrefl.mp irrefl hz) h

Premises used: Sym2.fromRel_irrefl, Iff.mp, Sym2.other_ne
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
hr : Symmetric r
f : α → β
h :
  ∀ (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
⊢ fromRel (r := Relation.Map r f f) ⋯ = map f '' fromRel (r := r) hr

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
hr : Symmetric r
f : α → β
x : Sym2 β
a b : β
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
⊢ Quot.mk (Rel β) (a, b) ∈ fromRel (r := Relation.Map r f f) ⋯ ↔ Quot.mk (Rel β) (a, b) ∈ map f '' fromRel (r := r) hr

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]

Premises used: Sym2.eq, and_or_left, exists_or, Sym2.exists, and_imp, Set.mem_image, forall_exists_index, Prod.swap_prod_mk, iff_self_or, Sym2.rel_iff', Sym2.map_mk, Prod.mk.injEq, Sym2.fromRel_prop, Relation.Map
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
hr : Symmetric r
f : α → β
x : Sym2 β
a b : β
⊢ ∀ (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:
fun c d hcd hc hd ↦ ⟨d, c, hr hcd, hd, hc⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
hr : Symmetric r
f : α → β
x : Sym2 β
a b : β
⊢ ∀ (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:
exact fun c d hcd hc hd ↦ ⟨d, c, hr hcd, hd, hc⟩
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
s : Set (Sym2 α)
x y : α
⊢ ToRel s x y ↔ s(x, y) ∈ s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Sym2.ToRel
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
s : Set (Sym2 α)
x y : α
⊢ ToRel s x y → ToRel s y x

Tactic:
simp [eq_swap]

Premises used: Sym2.eq_swap
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r : α → α → Prop
sym : Symmetric r
⊢ ToRel (fromRel (r := r) sym) = r

Tactic:
rfl

Premises used: Set.Mem, setOf, Sym2.fromRel, rfl, Sym2.ToRel
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
s : Set (Sym2 α)
⊢ fromRel (r := ToRel s) ⋯ = s

Tactic:
Set.ext fun z => Sym2.ind (fun _ _ => Iff.rfl) z

Premises used: Set.ext, Sym2.ind
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
s₁ s₂ : Set (Sym2 α)
⊢ ToRel s₁ ≤ ToRel s₂ ↔ s₁ ⊆ s₂

Tactic:
⟨(Sym2.ind ·), (@· s(·, ·))⟩

Premises used: Sym2.ind, Iff.intro
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
r_1 r₁ r₂ : α → α → Prop
r : { r : α → α → Prop // Symmetric r }
⊢ (fun (s : Set (Sym2 α)) ↦ Subtype.mk (p := fun (r : α → α → Prop) ↦ Symmetric r) (ToRel s) ⋯)
      ((fun (r : { r : α → α → Prop // Symmetric r }) ↦ fromRel (r := (↑r : α → α → Prop)) ⋯) r) =
    r

Tactic:
simp [toRel_fromRel]

Premises used: Sym2.toRel_fromRel
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
r r₁ r₂ : α → α → Prop
s : Set (Sym2 α)
⊢ (fun (r : { r : α → α → Prop // Symmetric r }) ↦ fromRel (r := (↑r : α → α → Prop)) ⋯)
      ((fun (s : Set (Sym2 α)) ↦ Subtype.mk (p := fun (r : α → α → Prop) ↦ Symmetric r) (ToRel s) ⋯) s) =
    s

Tactic:
simp [fromRel_toRel]

Premises used: Sym2.fromRel_toRel
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
r r₁_1 r₂_1 : α → α → Prop
r₁ r₂ : { r : α → α → Prop // Symmetric r }
⊢ LE.le (α := Set (Sym2 α))
      (({ toFun := fun (r : { r : α → α → Prop // Symmetric r }) ↦ fromRel (r := (↑r : α → α → Prop)) ⋯,
              invFun := fun (s : Set (Sym2 α)) ↦ Subtype.mk (p := fun (r : α → α → Prop) ↦ Symmetric r) (ToRel s) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { r : α → α → Prop // Symmetric r }) → Set (Sym2 α))
          r₁ :
        Set (Sym2 α))
      (({ toFun := fun (r : { r : α → α → Prop // Symmetric r }) ↦ fromRel (r := (↑r : α → α → Prop)) ⋯,
              invFun := fun (s : Set (Sym2 α)) ↦ Subtype.mk (p := fun (r : α → α → Prop) ↦ Symmetric r) (ToRel s) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : { r : α → α → Prop // Symmetric r }) → Set (Sym2 α))
          r₂ :
        Set (Sym2 α)) ↔
    r₁ ≤ r₂

Tactic:
simpa using fromRel_mono_iff ..

Premises used: Sym2.fromRel_mono_iff
-- Module: Mathlib.Data.Sym.Sym2
Goal:
α : Type u_1
r₁ r₂ : α → α → Prop
sym₁ : Symmetric r₁
sym₂ : Symmetric r₂
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 α))
⊢ fromRel (r := r₁) sym₁ = fromRel (r := r₂) sym₂ ↔ r₁ = r₂

Tactic:
rw [← Subtype.mk.injEq r₁ sym₁ r₂ sym₂, ← fromRelOrderIso α |>.eq_iff_eq]

Premises used: RelIso.eq_iff_eq, Sym2.fromRelOrderIso, Subtype.mk.injEq