awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
inst : DecidableEq α
i : α
β : α → Type u_10
f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))
fst :
  Prod.fst (β := (j : { j : α // j ≠ i }) → β (↑j : α))
      ((fun (f : (j : α) → β j) ↦
          ((f i, fun (j : { j : α // j ≠ i }) ↦ f (↑j : α)) : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))))
        ((fun (f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))) (j : α) ↦
            (if h : j = i then Eq.rec (motive := fun (x : α) (x_1 : i = x) ↦ β x) f.fst ⋯
              else f.snd (Subtype.mk (p := fun (j : α) ↦ j ≠ i) j h) :
              β j))
          f)) =
    f.fst
⊢ (fun (f : (j : α) → β j) ↦
        ((f i, fun (j : { j : α // j ≠ i }) ↦ f (↑j : α)) : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))))
      ((fun (f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))) (j : α) ↦
          (if h : j = i then Eq.rec (motive := fun (x : α) (x_1 : i = x) ↦ β x) f.fst ⋯
            else f.snd (Subtype.mk (p := fun (j : α) ↦ j ≠ i) j h) :
            β j))
        f) =
    f
have snd : ∀ (x : { j : α // j ≠ i }),
  Prod.snd (α := β i)
      ((fun (f : (j : α) → β j) ↦
          ((f i, fun (j : { j : α // j ≠ i }) ↦ f (↑j : α)) : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))))
        ((fun (f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))) (j : α) ↦
            (if h : j = i then Eq.rec (motive := fun (x : α) (x_1 : i = x) ↦ β x) f.fst sorry
              else f.snd (Subtype.mk (p := fun (j : α) ↦ j ≠ i) j h) :
              β j))
          f))
      x =
    f.snd x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set β
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑e.symm : (a : β) → α) '' s) ((⇑e : (a : α) → β) ⁻¹' s)
have h : ∀ (x : α),
  Membership.mem (γ := Set α) ((⇑e.symm : (a : β) → α) '' s) x ↔
    Membership.mem (γ := Set α) ((⇑e : (a : α) → β) ⁻¹' s) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
⊢ (⇑e.symm : (a : β) → α) '' t ⊆ s ↔ t ⊆ (⇑e : (a : α) → β) '' s
have rw : t ⊆ (⇑e.symm : (a : β) → α) ⁻¹' s ↔ t ⊆ (⇑e : (a : α) → β) '' s
Tactic: rw [image_subset_iff, image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
rw : t ⊆ (⇑e.symm : (a : β) → α) ⁻¹' s ↔ t ⊆ (⇑e : (a : α) → β) '' s
⊢ (⇑e.symm : (a : β) → α) '' t ⊆ s ↔ t ⊆ (⇑e : (a : α) → β) '' s
have rw₁ : t ⊆ (⇑e.symm : (a : β) → α) ⁻¹' s ↔ t ⊆ (⇑e.symm : (a : β) → α) ⁻¹' s
Tactic: rw [image_subset_iff, image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
⊢ s ⊆ (⇑e.symm : (a : β) → α) '' t ↔ (⇑e.symm.symm : (a : α) → β) '' s ⊆ t
have rw : s ⊆ (⇑e.symm : (a : β) → α) '' t ↔ s ⊆ (⇑e.symm : (a : β) → α) '' t
Tactic: rw [e.symm.symm_image_subset]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
⊢ (⇑e.symm.symm : (a : α) → β) '' s ⊆ t ↔ (⇑e : (a : α) → β) '' s ⊆ t
have rw : (⇑e : (a : α) → β) '' s ⊆ t ↔ (⇑e : (a : α) → β) '' s ⊆ t
Tactic: rw [e.symm_symm]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
p : α → Prop
⊢ Eq.{u_4 + 1} (α := Set β) {b : β | p ((e.symm : (a : β) → α) b)}
    (image.{u_3, u_4} (α := α) (⇑e : (a : α) → β) {a : α | p a})
have rw : Eq.{u_4 + 1} (α := Set β) {b : β | p ((e.symm : (a : β) → α) b)}
  (preimage.{u_4, u_3} (β := α) (⇑e.symm : (a : β) → α) {a : α | p a})
Tactic: rw [Equiv.image_eq_preimage_symm, preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
p : α → Prop
rw :
  Eq.{u_4 + 1} (α := Set β) {b : β | p ((e.symm : (a : β) → α) b)}
    (preimage.{u_4, u_3} (β := α) (⇑e.symm : (a : β) → α) {a : α | p a})
⊢ Eq.{u_4 + 1} (α := Set β) {b : β | p ((e.symm : (a : β) → α) b)}
    (image.{u_3, u_4} (α := α) (⇑e : (a : α) → β) {a : α | p a})
have rw₁ : Eq.{u_4 + 1} (α := Set β) {b : β | p ((e.symm : (a : β) → α) b)} {a : β | p ((e.symm : (a : β) → α) a)}
Tactic: rw [Equiv.image_eq_preimage_symm, preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
⊢ (⇑(prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
have h : ∀ (x : (α × β) × γ),
  Membership.mem (γ := Set ((α × β) × γ)) ((⇑(prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ t ×ˢ u) x ↔
    x ∈ (s ×ˢ t) ×ˢ u
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
⊢ (⇑(prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
have h : ∀ (x : α × β × γ),
  Membership.mem (γ := Set (α × β × γ)) ((⇑(prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) ⁻¹' (s ×ˢ t) ×ˢ u)
      x ↔
    x ∈ s ×ˢ t ×ˢ u
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
y : (↑((⇑e : (a : α) → β) '' s) : Type u_4)
⊢ Membership.mem (α := α) s ((e.symm : (a : β) → α) (↑y : β) : α)
have rcases : ∀ (a : α) (m : a ∈ s),
  Membership.mem (α := α) s
    ((e.symm : (a : β) → α)
        ((↑(Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑e : (a : α) → β) '' s) x)
                ((e : (a : α) → β) a) sorry) :
            β) :
          β) :
      α)
Tactic: rcases y with ⟨-, ⟨a, ⟨m, rfl⟩⟩⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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
⊢ (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'
have 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 : α) sorry
          | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) sorry :
          (↑(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 : α) sorry)
            else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) sorry) :
            (↑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
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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'
⊢ (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'
have 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 : α) sorry
          | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) sorry :
          (↑(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 : α) sorry)
            else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) sorry) :
            (↑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
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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)
⊢ (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
have 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 : α) sorry)
          else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) sorry) :
          (↑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 : α) sorry
            | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) sorry :
            (↑(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: rcases o with (⟨x, h⟩ | ⟨x, h⟩)
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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))
⊢ (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
have 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 : α) sorry)
          else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) sorry) :
          (↑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 : α) sorry
            | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) sorry :
            (↑(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: rcases o with (⟨x, h⟩ | ⟨x, h⟩)
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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)
⊢ (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
have 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 : α) sorry)
          else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) sorry) :
          (↑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 : α) sorry
            | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) sorry :
            (↑(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: rcases o with (⟨x, h⟩ | ⟨x, h⟩) <;> [simp [hs _ h]; simp [ht _ h]]
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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))
⊢ (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
have 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 : α) sorry)
          else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) sorry) :
          (↑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 : α) sorry
            | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) sorry :
            (↑(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: rcases o with (⟨x, h⟩ | ⟨x, h⟩) <;> [simp [hs _ h]; simp [ht _ h]]
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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
⊢ (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
have subst : (fun (x : PUnit.{u}) ↦ Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {a} x) a sorry)
    ((fun (x : (↑{a} : Type u_3)) ↦ PUnit.unit.{u})
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {a} x) a sorry)) =
  Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) {a} x) a sorry
Tactic: subst x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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 (α := (↑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))
have 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))
Tactic: apply (Equiv.Set.sumDiffSubset h).injective
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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 (α := (↑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))
have 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 : α) sorry)) :
    (↑t : Type u_3))
Tactic: apply (Equiv.Set.sumDiffSubset h).injective
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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
⊢ (↑(s ∪ t) : Type u) ⊕ (↑(s ∩ t) : Type u) ≃ (↑(s ∪ t \ s) : Type u) ⊕ (↑(s ∩ t) : Type u)
have rw : (↑(s ∪ t) : Type u) ⊕ (↑(s ∩ t) : Type u) ≃ (↑(s ∪ t) : Type u) ⊕ (↑(s ∩ t) : Type u)
Tactic: rw [union_diff_self]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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
⊢ (↑(t \ s) : Type u) ⊕ (↑(s ∩ t) : Type u) ≃ (↑(t \ s ∪ s ∩ t) : Type u)
have refine_1 : ∀ (x : α), x ∈ t \ s → (fun (x : α) ↦ ¬x ∈ s) x
Tactic: refine (Set.union' (· ∉ s) ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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
⊢ (↑(t \ s) : Type u) ⊕ (↑(s ∩ t) : Type u) ≃ (↑(t \ s ∪ s ∩ t) : Type u)
have refine_2 : ∀ (x : α), x ∈ s ∩ t → ¬(fun (x : α) ↦ ¬x ∈ s) x
Tactic: refine (Set.union' (· ∉ s) ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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
⊢ (↑s : Type u) ⊕ (↑(t \ s ∪ s ∩ t) : Type u) ≃ (↑s : Type u) ⊕ (↑t : Type u)
have rw : t \ s ∪ s ∩ t = t
Tactic: rw [(_ : t \ s ∪ s ∩ t = t)]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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
⊢ t \ s ∪ s ∩ t = t
have rw : s ∩ t ∪ t \ s = t
Tactic: rw [union_comm, inter_comm, inter_union_diff]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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 : s ∩ t ∪ t \ s = t
⊢ t \ s ∪ s ∩ t = t
have rw₁ : t ∩ s ∪ t \ s = t
Tactic: rw [union_comm, inter_comm, inter_union_diff]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
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 : s ∩ t ∪ t \ s = t
rw₁ : t ∩ s ∪ t \ s = t
⊢ t \ s ∪ s ∩ t = t
have rw₂ : t = t
Tactic: rw [union_comm, inter_comm, inter_union_diff]