awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
s t : Set α
p : α → Prop
inst : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x_1 : (↑(s ∪ t) : Type u_3)
x : α
h' : x ∈ s ∪ t
pos :
  ∀ (h : p x),
    (fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
          (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
            | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
            | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
            (↑(s ∪ t) : Type u_3)))
        ((fun (x : (↑(s ∪ t) : Type u_3)) ↦
            (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
              else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
              (↑s : Type u_3) ⊕ (↑t : Type u_3)))
          (Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) x h')) =
      Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) x h'
neg :
  ∀ (h : ¬p x),
    (fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
          (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
            | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
            | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
            (↑(s ∪ t) : Type u_3)))
        ((fun (x : (↑(s ∪ t) : Type u_3)) ↦
            (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
              else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
              (↑s : Type u_3) ⊕ (↑t : Type u_3)))
          (Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) x h')) =
      Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) x h'
⊢ (fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
        (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
          | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
          | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
          (↑(s ∪ t) : Type u_3)))
      ((fun (x : (↑(s ∪ t) : Type u_3)) ↦
          (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
            else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
            (↑s : Type u_3) ⊕ (↑t : Type u_3)))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) x h')) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) x h'

Tactic:
by_cases h : p x
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
s t : Set α
p : α → Prop
inst : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x_1 : (↑(s ∪ t) : Type u_3)
x : α
h' : x ∈ s ∪ t
h : p x
⊢ (fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
        (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
          | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
          | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
          (↑(s ∪ t) : Type u_3)))
      ((fun (x : (↑(s ∪ t) : Type u_3)) ↦
          (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
            else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
            (↑s : Type u_3) ⊕ (↑t : Type u_3)))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) x h')) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) x h'

Tactic:
simp [h]
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
s t : Set α
p : α → Prop
inst : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x_1 : (↑(s ∪ t) : Type u_3)
x : α
h' : x ∈ s ∪ t
h : ¬p x
⊢ (fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
        (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
          | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
          | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
          (↑(s ∪ t) : Type u_3)))
      ((fun (x : (↑(s ∪ t) : Type u_3)) ↦
          (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
            else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
            (↑s : Type u_3) ⊕ (↑t : Type u_3)))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) x h')) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) x h'

Tactic:
simp [h]
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
s t : Set α
p : α → Prop
inst : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
o : (↑s : Type u_3) ⊕ (↑t : Type u_3)
inl :
  ∀ (x : α) (h : x ∈ s),
    Eq (α := (↑s : Type u_3) ⊕ (↑t : Type u_3))
      ((fun (x : (↑(s ∪ t) : Type u_3)) ↦
          (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
            else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
            (↑s : Type u_3) ⊕ (↑t : Type u_3)))
        ((fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
            (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
              | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
              | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
              (↑(s ∪ t) : Type u_3)))
          (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h))))
      (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h))
inr :
  ∀ (x : α) (h : x ∈ t),
    Eq (α := (↑s : Type u_3) ⊕ (↑t : Type u_3))
      ((fun (x : (↑(s ∪ t) : Type u_3)) ↦
          (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
            else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
            (↑s : Type u_3) ⊕ (↑t : Type u_3)))
        ((fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
            (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
              | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
              | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
              (↑(s ∪ t) : Type u_3)))
          (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x h))))
      (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x h))
⊢ (fun (x : (↑(s ∪ t) : Type u_3)) ↦
        (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
          else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
          (↑s : Type u_3) ⊕ (↑t : Type u_3)))
      ((fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
          (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
            | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
            | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
            (↑(s ∪ t) : Type u_3)))
        o) =
    o

Tactic:
rcases o with (⟨x, h⟩ | ⟨x, h⟩)
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
s t : Set α
p : α → Prop
inst : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x : α
h : x ∈ s
⊢ Eq (α := (↑s : Type u_3) ⊕ (↑t : Type u_3))
    ((fun (x : (↑(s ∪ t) : Type u_3)) ↦
        (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
          else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
          (↑s : Type u_3) ⊕ (↑t : Type u_3)))
      ((fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
          (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
            | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
            | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
            (↑(s ∪ t) : Type u_3)))
        (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h))))
    (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h))

Tactic:
simp [hs _ h]
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
s t : Set α
p : α → Prop
inst : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x : α
h : x ∈ t
⊢ Eq (α := (↑s : Type u_3) ⊕ (↑t : Type u_3))
    ((fun (x : (↑(s ∪ t) : Type u_3)) ↦
        (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
          else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
          (↑s : Type u_3) ⊕ (↑t : Type u_3)))
      ((fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
          (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
            | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
            | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
            (↑(s ∪ t) : Type u_3)))
        (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x h))))
    (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x h))

Tactic:
simp [ht _ h]
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
H : Disjoint s t
a : (↑(s ∪ t) : Type u_3)
ha : (↑a : α) ∈ s
⊢ Eq (α := (↑s : Type u_3) ⊕ (↑t : Type u_3))
    ((Set.union (s := s) (t := t) H : (a : (↑(s ∪ t) : Type u_3)) → (↑s : Type u_3) ⊕ (↑t : Type u_3)) a :
      (↑s : Type u_3) ⊕ (↑t : Type u_3))
    (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑a : α) ha) : (↑s : Type u_3) ⊕ (↑t : Type u_3))

Tactic:
dif_pos ha

Premises used: dif_pos, dite
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
H : Disjoint s t
a : (↑(s ∪ t) : Type u_3)
ha : (↑a : α) ∈ t
⊢ Eq (α := (↑s : Type u_3) ⊕ (↑t : Type u_3))
    ((Set.union (s := s) (t := t) H : (a : (↑(s ∪ t) : Type u_3)) → (↑s : Type u_3) ⊕ (↑t : Type u_3)) a :
      (↑s : Type u_3) ⊕ (↑t : Type u_3))
    (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑a : α) ha) : (↑s : Type u_3) ⊕ (↑t : Type u_3))

Tactic:
dif_neg fun h => Set.disjoint_left.mp H h ha

Premises used: Set.disjoint_left, dif_neg, dite, Iff.mp
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
H : Disjoint s t
a : (↑s : Type u_3)
⊢ (↑a : α) ∈ s ∪ t

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
H : Disjoint s t
a : (↑s : Type u_3)
⊢ Eq (α := (↑(s ∪ t) : Type u_3))
    (((Set.union (s := s) (t := t) H).symm : (a : (↑s : Type u_3) ⊕ (↑t : Type u_3)) → (↑(s ∪ t) : Type u_3))
        (Sum.inl a) :
      (↑(s ∪ t) : Type u_3))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑a : α) ⋯ : { x : α // x ∈ s ∪ t })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
H : Disjoint s t
a : (↑t : Type u_3)
⊢ (↑a : α) ∈ s ∪ t

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
H : Disjoint s t
a : (↑t : Type u_3)
⊢ Eq (α := (↑(s ∪ t) : Type u_3))
    (((Set.union (s := s) (t := t) H).symm : (a : (↑s : Type u_3) ⊕ (↑t : Type u_3)) → (↑(s ∪ t) : Type u_3))
        (Sum.inr a) :
      (↑(s ∪ t) : Type u_3))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑a : α) ⋯ : { x : α // x ∈ s ∪ t })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
a : α
x_1 : (↑{a} : Type u_3)
x : α
h : Membership.mem (γ := Set α) {a} x
subst :
  (fun (x : PUnit.{u}) ↦ Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {a} x) a ⋯)
      ((fun (x : (↑{a} : Type u_3)) ↦ PUnit.unit.{u})
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {a} x) a ⋯)) =
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {a} x) a ⋯
⊢ (fun (x : PUnit.{u}) ↦ Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {a} x) a ⋯)
      ((fun (x : (↑{a} : Type u_3)) ↦ PUnit.unit.{u})
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {a} x) x h)) =
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {a} x) x h

Tactic:
subst x
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
a : α
x : (↑{a} : Type u_3)
⊢ (fun (x : PUnit.{u}) ↦ Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {a} x) a ⋯)
      ((fun (x : (↑{a} : Type u_3)) ↦ PUnit.unit.{u})
        (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {a} x) a ⋯)) =
    Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {a} x) a ⋯

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
inst : Preorder α
S T : Set α
h : S = T
⊢ StrictMono (α := (↑S : Type u_3)) (β := (↑T : Type u_3))
    (⇑(setCongr (s := S) (t := T) h) : (a : (↑S : Type u_3)) → (↑T : Type u_3))

Tactic:
fun _ _ ↦ id

Premises used: StrictMono, Set.Mem, id
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
H : ¬a ∈ s
⊢ insert a s = s ∪ {a}

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
H : ¬a ∈ s
⊢ Disjoint s {a}

Tactic:
simpa
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
H : ¬a ∈ s
b : (↑s : Type u)
⊢ Eq (α := (↑(insert a s) : Type u))
    (((Set.insert (s := s) H).symm : (a_1 : (↑s : Type u) ⊕ PUnit) → (↑(insert a s) : Type u)) (Sum.inl b) :
      (↑(insert a s) : Type u))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) (↑b : α) ⋯ : { x : α // x ∈ insert a s })

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
H : ¬a ∈ s
b : PUnit
⊢ Eq (α := (↑(insert a s) : Type u))
    (((Set.insert (s := s) H).symm : (a_1 : (↑s : Type u) ⊕ PUnit) → (↑(insert a s) : Type u)) (Sum.inr b) :
      (↑(insert a s) : Type u))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) a ⋯ : { x : α // x ∈ insert a s })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
H : ¬a ∈ s
⊢ Eq (α := (↑s : Type u) ⊕ PUnit)
    ((Set.insert (s := s) H : (a : (↑(insert a s) : Type u)) → (↑s : Type u) ⊕ PUnit)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) a ⋯) :
      (↑s : Type u) ⊕ PUnit)
    (Sum.inr PUnit.unit : (↑s : Type u) ⊕ PUnit)

Tactic:
(Equiv.Set.insert H).apply_eq_iff_eq_symm_apply.2 rfl

Premises used: Iff.mpr, Equiv.Set.insert, rfl, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
H : ¬a ∈ s
b : (↑s : Type u)
⊢ Eq (α := (↑s : Type u) ⊕ PUnit)
    ((Set.insert (s := s) H : (a : (↑(insert a s) : Type u)) → (↑s : Type u) ⊕ PUnit)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) (↑b : α) ⋯) :
      (↑s : Type u) ⊕ PUnit)
    (Sum.inl b : (↑s : Type u) ⊕ PUnit)

Tactic:
(Equiv.Set.insert H).apply_eq_iff_eq_symm_apply.2 rfl

Premises used: Iff.mpr, Equiv.Set.insert, rfl, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
x : (↑s : Type u)
⊢ (Set.sumCompl s : (a : (↑s : Type u) ⊕ (↑sᶜ : Type u)) → α) (Sum.inl x) = (↑x : α)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
x : (↑sᶜ : Type u)
⊢ (Set.sumCompl s : (a : (↑s : Type u) ⊕ (↑sᶜ : Type u)) → α) (Sum.inr x) = (↑x : α)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
x : α
hx : x ∈ s
⊢ Eq (α := (↑s : Type u) ⊕ (↑sᶜ : Type u))
    (((Set.sumCompl s).symm : (a : α) → (↑s : Type u) ⊕ (↑sᶜ : Type u)) x : (↑s : Type u) ⊕ (↑sᶜ : Type u))
    (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) : (↑s : Type u) ⊕ (↑sᶜ : Type u))

Tactic:
sumCompl_symm_apply_of_pos hx

Premises used: Set.Mem, setOf, Not, Equiv.sumCompl_symm_apply_of_pos
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
x : α
hx : ¬x ∈ s
⊢ Eq (α := (↑s : Type u) ⊕ (↑sᶜ : Type u))
    (((Set.sumCompl s).symm : (a : α) → (↑s : Type u) ⊕ (↑sᶜ : Type u)) x : (↑s : Type u) ⊕ (↑sᶜ : Type u))
    (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ sᶜ) x hx) : (↑s : Type u) ⊕ (↑sᶜ : Type u))

Tactic:
sumCompl_symm_apply_of_neg hx

Premises used: Set.Mem, setOf, Not, Equiv.sumCompl_symm_apply_of_neg
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
x : (↑s : Type u_3)
⊢ Eq (α := (↑s : Type u_3) ⊕ (↑sᶜ : Type u_3))
    (((Set.sumCompl s).symm : (a : α) → (↑s : Type u_3) ⊕ (↑sᶜ : Type u_3)) (↑x : α) :
      (↑s : Type u_3) ⊕ (↑sᶜ : Type u_3))
    (Sum.inl x : (↑s : Type u_3) ⊕ (↑sᶜ : Type u_3))

Tactic:
sumCompl_symm_apply_pos x

Premises used: Equiv.sumCompl_symm_apply_pos, Set.Mem, setOf, Not
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
x : (↑sᶜ : Type u_3)
⊢ Eq (α := (↑s : Type u_3) ⊕ (↑sᶜ : Type u_3))
    (((Set.sumCompl s).symm : (a : α) → (↑s : Type u_3) ⊕ (↑sᶜ : Type u_3)) (↑x : α) :
      (↑s : Type u_3) ⊕ (↑sᶜ : Type u_3))
    (Sum.inr x : (↑s : Type u_3) ⊕ (↑sᶜ : Type u_3))

Tactic:
sumCompl_symm_apply_neg x

Premises used: Set.Mem, setOf, Equiv.sumCompl_symm_apply_neg, Not
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
s t : Set α
h : s ⊆ t
inst : DecidablePred fun (x : α) ↦ x ∈ s
⊢ s ∪ t \ s = t

Tactic:
simp [union_diff_self, union_eq_self_of_subset_left h]

Premises used: Set.union_eq_self_of_subset_left, Set.union_diff_self
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
s t : Set α
h : s ⊆ t
inst : DecidablePred fun (x : α) ↦ x ∈ s
x : (↑s : Type u_3)
⊢ (Set.sumDiffSubset (s := s) (t := t) h : (a : (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3)) → (↑t : Type u_3))
      (Sum.inl x) =
    inclusion (s := s) (t := t) h x

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
s t : Set α
h : s ⊆ t
inst : DecidablePred fun (x : α) ↦ x ∈ s
x : (↑(t \ s) : Type u_3)
⊢ (Set.sumDiffSubset (s := s) (t := t) h : (a : (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3)) → (↑t : Type u_3))
      (Sum.inr x) =
    inclusion (s := t \ s) (t := t) ⋯ x

Tactic:
rfl

Premises used: Set.Mem, Set.diff, setOf, rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
s t : Set α
h : s ⊆ t
inst : DecidablePred fun (x : α) ↦ x ∈ s
x : (↑t : Type u_3)
hx : (↑x : α) ∈ s
a :
  Eq (α := (↑t : Type u_3))
    ((Set.sumDiffSubset (s := s) (t := t) h : (a : (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3)) → (↑t : Type u_3))
        (((Set.sumDiffSubset (s := s) (t := t) h).symm :
            (a : (↑t : Type u_3)) → (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3))
          x) :
      (↑t : Type u_3))
    ((Set.sumDiffSubset (s := s) (t := t) h : (a : (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3)) → (↑t : Type u_3))
        (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) hx)) :
      (↑t : Type u_3))
⊢ Eq (α := (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3))
    (((Set.sumDiffSubset (s := s) (t := t) h).symm : (a : (↑t : Type u_3)) → (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3))
        x :
      (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3))
    (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) hx) : (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3))

Tactic:
apply (Equiv.Set.sumDiffSubset h).injective

Premises used: Equiv.injective, Equiv.Set.sumDiffSubset
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
s t : Set α
h : s ⊆ t
inst : DecidablePred fun (x : α) ↦ x ∈ s
x : (↑t : Type u_3)
hx : (↑x : α) ∈ s
⊢ Eq (α := (↑t : Type u_3))
    ((Set.sumDiffSubset (s := s) (t := t) h : (a : (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3)) → (↑t : Type u_3))
        (((Set.sumDiffSubset (s := s) (t := t) h).symm :
            (a : (↑t : Type u_3)) → (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3))
          x) :
      (↑t : Type u_3))
    ((Set.sumDiffSubset (s := s) (t := t) h : (a : (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3)) → (↑t : Type u_3))
        (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) hx)) :
      (↑t : Type u_3))

Tactic:
simp only [apply_symm_apply, sumDiffSubset_apply_inl, Set.inclusion_mk]

Premises used: Equiv.apply_symm_apply, Equiv.Set.sumDiffSubset_apply_inl, Set.inclusion_mk
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
s t : Set α
h : s ⊆ t
inst : DecidablePred fun (x : α) ↦ x ∈ s
x : (↑t : Type u_3)
hx : ¬(↑x : α) ∈ s
a :
  Eq (α := (↑t : Type u_3))
    ((Set.sumDiffSubset (s := s) (t := t) h : (a : (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3)) → (↑t : Type u_3))
        (((Set.sumDiffSubset (s := s) (t := t) h).symm :
            (a : (↑t : Type u_3)) → (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3))
          x) :
      (↑t : Type u_3))
    ((Set.sumDiffSubset (s := s) (t := t) h : (a : (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3)) → (↑t : Type u_3))
        (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t \ s) (↑x : α) ⋯)) :
      (↑t : Type u_3))
⊢ Eq (α := (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3))
    (((Set.sumDiffSubset (s := s) (t := t) h).symm : (a : (↑t : Type u_3)) → (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3))
        x :
      (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3))
    (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t \ s) (↑x : α) ⋯) : (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3))

Tactic:
apply (Equiv.Set.sumDiffSubset h).injective

Premises used: Equiv.injective, Equiv.Set.sumDiffSubset
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
s t : Set α
h : s ⊆ t
inst : DecidablePred fun (x : α) ↦ x ∈ s
x : (↑t : Type u_3)
hx : ¬(↑x : α) ∈ s
⊢ Eq (α := (↑t : Type u_3))
    ((Set.sumDiffSubset (s := s) (t := t) h : (a : (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3)) → (↑t : Type u_3))
        (((Set.sumDiffSubset (s := s) (t := t) h).symm :
            (a : (↑t : Type u_3)) → (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3))
          x) :
      (↑t : Type u_3))
    ((Set.sumDiffSubset (s := s) (t := t) h : (a : (↑s : Type u_3) ⊕ (↑(t \ s) : Type u_3)) → (↑t : Type u_3))
        (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t \ s) (↑x : α) ⋯)) :
      (↑t : Type u_3))

Tactic:
simp only [apply_symm_apply, sumDiffSubset_apply_inr, Set.inclusion_mk]

Premises used: Equiv.apply_symm_apply, Equiv.Set.sumDiffSubset_apply_inr, Set.inclusion_mk
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
rw rw₁ : (↑(s ∪ t) : Type u) ⊕ (↑(s ∩ t) : Type u) ≃ (↑(s ∪ t) : Type u) ⊕ (↑(s ∩ t) : Type u)
⊢ (↑(s ∪ t) : Type u) ⊕ (↑(s ∩ t) : Type u) ≃ (↑(s ∪ t \ s) : Type u) ⊕ (↑(s ∩ t) : Type u)

Tactic:
rw [union_diff_self]

Premises used: Set.union_diff_self
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
refine_1 : ∀ (x : α), x ∈ t \ s → (fun (x : α) ↦ ¬x ∈ s) x
refine_2 : ∀ (x : α), x ∈ s ∩ t → ¬(fun (x : α) ↦ ¬x ∈ s) x
⊢ (↑(t \ s) : Type u) ⊕ (↑(s ∩ t) : Type u) ≃ (↑(t \ s ∪ s ∩ t) : Type u)

Tactic:
refine (Set.union' (· ∉ s) ?_ ?_).symm

Premises used: Equiv.Set.union', Membership.mem, Equiv.symm, Not
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
⊢ ∀ (x : α), x ∈ t \ s → (fun (x : α) ↦ ¬x ∈ s) x

Tactic:
fun x hx => hx.2

Premises used: And.right
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
⊢ ∀ (x : α), x ∈ s ∩ t → ¬(fun (x : α) ↦ ¬x ∈ s) x

Tactic:
fun x hx => not_not_intro hx.1

Premises used: not_not_intro, And.left