awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (↑s : Type u) ⊕ (↑t : Type u) ≃ (↑s : Type u) ⊕ (↑t : Type u)
Tactic: { rw [(_ : t \ s ∪ s ∩ t = t)]
        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 : Type u) ⊕ (↑t : Type u) ≃ (↑s : Type u) ⊕ (↑t : Type u)
⊢ (↑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)]
        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
β_2 : Type u_2
α : Type u
β : Type v
s : Set α
t : Set β
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : DecidablePred fun (x : β) ↦ x ∈ t
e₀ : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)
e :
  { e : α ≃ β //
    ∀ (x : (↑s : Type u)),
      Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β) ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }
⊢ (fun (e₁ : Equiv.{u + 1, v + 1} (↑sᶜ : Type u) (↑tᶜ : Type v)) ↦
        (Subtype.mk (p := fun (e : α ≃ β) ↦
            ∀ (x : (↑s : Type u)),
              Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β))
            (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (Set.sumCompl s).symm (e₀.sumCongr e₁))
              (Set.sumCompl t))
            ⋯ :
          { e : α ≃ β //
            ∀ (x : (↑s : Type u)),
              Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }))
      ((fun
            (e :
              { e : α ≃ β //
                ∀ (x : (↑s : Type u)),
                  Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                    ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }) ↦
          ((↑e : α ≃ β).subtypeEquiv (p := Membership.mem sᶜ) (q := Membership.mem tᶜ) ⋯ :
            Equiv.{u + 1, v + 1} { a : α // a ∈ sᶜ } { b : β // b ∈ tᶜ }))
        e) =
    e
have a : ∀ (x : α),
  Eq.{v + 1} (α := β)
    (((↑((fun (e₁ : Equiv.{u + 1, v + 1} (↑sᶜ : Type u) (↑tᶜ : Type v)) ↦
                  (Subtype.mk (p := fun (e : α ≃ β) ↦
                      ∀ (x : (↑s : Type u)),
                        Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                          ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β))
                      (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                        (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (Set.sumCompl s).symm (e₀.sumCongr e₁))
                        (Set.sumCompl t))
                      sorry :
                    { e : α ≃ β //
                      ∀ (x : (↑s : Type u)),
                        Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                          ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }))
                ((fun
                      (e :
                        { e : α ≃ β //
                          ∀ (x : (↑s : Type u)),
                            Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                              ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }) ↦
                    ((↑e : α ≃ β).subtypeEquiv (p := Membership.mem sᶜ) (q := Membership.mem tᶜ) sorry :
                      Equiv.{u + 1, v + 1} { a : α // a ∈ sᶜ } { b : β // b ∈ tᶜ }))
                  e)) :
            α ≃ β) :
          (a : α) → β)
        x :
      β)
    (((↑e : α ≃ β) : (a : α) → β) x : β)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
u s : Set α
⊢ Eq (α := Set (↑(f '' s) : Type u_4))
    ((fun (x : (↑(f '' s) : Type u_4)) ↦
        (↑(((Set.image f s hf).symm : (a : (↑(f '' s) : Type u_4)) → (↑s : Type u_3)) x) : α)) ⁻¹'
      u)
    (Subtype.val (p := fun (x : β) ↦ x ∈ f '' s) ⁻¹' f '' u)
have h : ∀ (a : α) (has : a ∈ s),
  Membership.mem (γ := Set (↑(f '' s) : Type u_4))
      ((fun (x : (↑(f '' s) : Type u_4)) ↦
          (↑(((Set.image f s hf).symm : (a : (↑(f '' s) : Type u_4)) → (↑s : Type u_3)) x) : α)) ⁻¹'
        u)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ f '' s) (f a) sorry) ↔
    Membership.mem (γ := Set (↑(f '' s) : Type u_4)) (Subtype.val (p := fun (x : β) ↦ x ∈ f '' s) ⁻¹' f '' u)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ f '' s) (f a) sorry)
Tactic: ext ⟨b, a, has, rfl⟩
-- 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 : Set α
x : (↑(𝒫 S) : Type u_3)
⊢ (fun (x : Set (↑S : Type u_3)) ↦
        Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝒫 S) (Subtype.val (p := fun (x : α) ↦ x ∈ S) '' x) ⋯)
      ((fun (x : (↑(𝒫 S) : Type u_3)) ↦ (Subtype.val (p := fun (x : α) ↦ x ∈ S) ⁻¹' (↑x : Set α) : Set (↑S : Type u_3)))
        x) =
    x
have a : ∀ (y : α),
  Membership.mem (γ := Set α)
      (↑((fun (x : Set (↑S : Type u_3)) ↦
              Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝒫 S) (Subtype.val (p := fun (x : α) ↦ x ∈ S) '' x) sorry)
            ((fun (x : (↑(𝒫 S) : Type u_3)) ↦
                (Subtype.val (p := fun (x : α) ↦ x ∈ S) ⁻¹' (↑x : Set α) : Set (↑S : Type u_3)))
              x)) :
        Set α)
      y ↔
    y ∈ (↑x : Set α)
Tactic: ext 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 : Set α
x : Set (↑S : Type u_3)
⊢ (fun (x : (↑(𝒫 S) : Type u_3)) ↦ (Subtype.val (p := fun (x : α) ↦ x ∈ S) ⁻¹' (↑x : Set α) : Set (↑S : Type u_3)))
      ((fun (x : Set (↑S : Type u_3)) ↦
          Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝒫 S) (Subtype.val (p := fun (x : α) ↦ x ∈ S) '' x) ⋯)
        x) =
    x
have h : ∀ (x_1 : (↑S : Type u_3)),
  Membership.mem (γ := Set (↑S : Type u_3))
      ((fun (x : (↑(𝒫 S) : Type u_3)) ↦ (Subtype.val (p := fun (x : α) ↦ x ∈ S) ⁻¹' (↑x : Set α) : Set (↑S : Type u_3)))
        ((fun (x : Set (↑S : Type u_3)) ↦
            Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝒫 S) (Subtype.val (p := fun (x : α) ↦ x ∈ S) '' x) sorry)
          x))
      x_1 ↔
    x_1 ∈ x
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
f : α → β
s : Set (↑(range f) : Type u_4)
x : (↑(rangeSplitting f '' s) : Type u_3)
⊢ Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f (↑x : α)) ⋯ ∈ s
have rcases : ∀ (y : (↑(range f) : Type u_4)) (m : y ∈ s),
  Subtype.mk (p := fun (x : β) ↦ x ∈ range f)
      (f (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f y) sorry) : α)) sorry ∈
    s
Tactic: rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩
Cleared hypotheses: x
-- 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
f : α → β
s : Set (↑(range f) : Type u_4)
x : (↑(rangeSplitting f '' s) : Type u_3)
⊢ (fun (x : (↑s : Type u_4)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f (↑x : (↑(range f) : Type u_4))) ⋯ :
          { x : α // x ∈ rangeSplitting f '' s }))
      ((fun (x : (↑(rangeSplitting f '' s) : Type u_3)) ↦
          Subtype.mk (p := fun (x : (↑(range f) : Type u_4)) ↦ x ∈ s)
            (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f (↑x : α)) ⋯) ⋯)
        x) =
    x
have rcases : ∀ (y : (↑(range f) : Type u_4)) (m : y ∈ s),
  Eq (α := (↑(rangeSplitting f '' s) : Type u_3))
    ((fun (x : (↑s : Type u_4)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f (↑x : (↑(range f) : Type u_4))) sorry :
          { x : α // x ∈ rangeSplitting f '' s }))
      ((fun (x : (↑(rangeSplitting f '' s) : Type u_3)) ↦
          Subtype.mk (p := fun (x : (↑(range f) : Type u_4)) ↦ x ∈ s)
            (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f (↑x : α)) sorry) sorry)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f y) sorry)))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f y) sorry)
Tactic: rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩
Cleared hypotheses: x
-- 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
val : β
h : Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) (Sum.inr val)
⊢ False
have rcases : ∀ (x : α) (h' : Sum.inl x = Sum.inr val), False
Tactic: rcases h with ⟨x, h'⟩
Cleared hypotheses: h
-- 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
val : α
h : Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) (Sum.inl val)
⊢ False
have rcases : ∀ (x : β) (h' : Sum.inr x = Sum.inl val), False
Tactic: rcases h with ⟨x, h'⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Sort u_3
β : Type u_4
f : α → β
hf : Injective f
a : α
⊢ ((ofInjective f hf).symm : (a : (↑(range f) : Type u_4)) → α) (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f a) ⋯) =
    a
have a₁ : Eq.{u_4 + 1} (α := (↑(range f) : Type u_4))
  ((ofInjective f hf : (a : α) → (↑(range f) : Type u_4))
      (((ofInjective f hf).symm : (a : (↑(range f) : Type u_4)) → α)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f a) sorry)) :
    (↑(range f) : Type u_4))
  ((ofInjective f hf : (a : α) → (↑(range f) : Type u_4)) a : (↑(range f) : Type u_4))
Tactic: apply (ofInjective f hf).injective
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ (⇑(ofInjective f hf).symm : (a : (↑(range f) : Type u_4)) → α) = rangeSplitting f
have h : ∀ (x : α),
  ((ofInjective f hf).symm : (a : (↑(range f) : Type u_4)) → α) (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) sorry) =
    rangeSplitting f (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) sorry)
Tactic: ext ⟨y, x, rfl⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
x : α
⊢ ((ofInjective f hf).symm : (a : (↑(range f) : Type u_4)) → α) (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) ⋯) =
    rangeSplitting f (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) ⋯)
have h : f
    (((ofInjective f hf).symm : (a : (↑(range f) : Type u_4)) → α)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) sorry)) =
  f (rangeSplitting f (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) sorry))
Tactic: apply hf
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : Type u_4
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
⊢ ofLeftInverse f f_inv hf = ofInjective f ⋯
have H : ∀ (x : α),
  Eq.{u_4 + 1} (α := β) (↑((ofLeftInverse f f_inv hf : (a : α) → (↑(range f) : Type u_4)) x) : β)
    (↑((ofInjective f sorry : (a : α) → (↑(range f) : Type u_4)) x) : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : Type u_4
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
⊢ ofLeftInverse' f f_inv hf = ofInjective f ⋯
have H : ∀ (x : α),
  Eq.{u_4 + 1} (α := β) (↑((ofLeftInverse' f f_inv hf : (a : α) → (↑(range f) : Type u_4)) x) : β)
    (↑((ofInjective f sorry : (a : α) → (↑(range f) : Type u_4)) x) : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : α → Type u_4
p : α → Prop
inst : DecidablePred p
s : (i : α) → Set (β i)
⊢ (⇑(piEquivPiSubtypeProd p β).symm :
        (a : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) → (i : α) → β i) ⁻¹'
      pi (α := β) univ s =
    SProd.sprod (α := Set ((i : { i : α // p i }) → β (↑i : α))) (β := Set ((i : { i : α // ¬p i }) → β (↑i : α)))
      (pi (α := fun (i : { i : α // p i }) ↦ β (↑i : α)) univ fun (i : { i : α // p i }) ↦ s (↑i : α))
      (pi (α := fun (i : { i : α // ¬p i }) ↦ β (↑i : α)) univ fun (i : { i : α // ¬p i }) ↦ s (↑i : α))
have h : ∀ (f : (i : { x : α // p x }) → β (↑i : α)) (g : (i : { x : α // ¬p x }) → β (↑i : α)),
  Membership.mem (γ := Set (((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))))
      ((⇑(piEquivPiSubtypeProd p β).symm :
          (a : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) → (i : α) → β i) ⁻¹'
        pi (α := β) univ s)
      (f, g) ↔
    (f, g) ∈
      SProd.sprod (α := Set ((i : { i : α // p i }) → β (↑i : α))) (β := Set ((i : { i : α // ¬p i }) → β (↑i : α)))
        (pi (α := fun (i : { i : α // p i }) ↦ β (↑i : α)) univ fun (i : { i : α // p i }) ↦ s (↑i : α))
        (pi (α := fun (i : { i : α // ¬p i }) ↦ β (↑i : α)) univ fun (i : { i : α // ¬p i }) ↦ s (↑i : α))
Tactic: ext ⟨f, g⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : α → Type u_4
p : α → Prop
inst : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x : α // p x }) → β (↑i : α)
g : (i : { x : α // ¬p x }) → β (↑i : α)
⊢ Membership.mem (γ := Set (((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))))
      ((⇑(piEquivPiSubtypeProd p β).symm :
          (a : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) → (i : α) → β i) ⁻¹'
        pi (α := β) univ s)
      (f, g) ↔
    (f, g) ∈
      SProd.sprod (α := Set ((i : { i : α // p i }) → β (↑i : α))) (β := Set ((i : { i : α // ¬p i }) → β (↑i : α)))
        (pi (α := fun (i : { i : α // p i }) ↦ β (↑i : α)) univ fun (i : { i : α // p i }) ↦ s (↑i : α))
        (pi (α := fun (i : { i : α // ¬p i }) ↦ β (↑i : α)) univ fun (i : { i : α // ¬p i }) ↦ s (↑i : α))
have h : (∀ (i : α),
    Membership.mem (α := β i) (s i)
      (((piEquivPiSubtypeProd p β).symm :
            (a : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) → (i : α) → β i)
          (f, g) i :
        β i)) ↔
  ∀ (x : α),
    (∀ (b : p x), f (Subtype.mk (p := fun (a : α) ↦ p a) x b) ∈ s x) ∧
      ∀ (b : ¬p x), g (Subtype.mk (p := fun (a : α) ↦ ¬p a) x b) ∈ s x
Tactic: simp only [mem_preimage, mem_univ_pi, prodMk_mem_set_prod_eq, Subtype.forall, ← forall_and]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : α → Type u_4
p : α → Prop
inst : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x : α // p x }) → β (↑i : α)
g : (i : { x : α // ¬p x }) → β (↑i : α)
⊢ (∀ (i : α),
      Membership.mem (α := β i) (s i)
        (((piEquivPiSubtypeProd p β).symm :
              (a : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) → (i : α) → β i)
            (f, g) i :
          β i)) ↔
    ∀ (x : α),
      (∀ (b : p x), f (Subtype.mk (p := fun (a : α) ↦ p a) x b) ∈ s x) ∧
        ∀ (b : ¬p x), g (Subtype.mk (p := fun (a : α) ↦ ¬p a) x b) ∈ s x
have h : ∀ (i : α),
  Membership.mem (α := β i) (s i)
      (((piEquivPiSubtypeProd p β).symm :
            (a : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) → (i : α) → β i)
          (f, g) i :
        β i) ↔
    (∀ (b : p i), f (Subtype.mk (p := fun (a : α) ↦ p a) i b) ∈ s i) ∧
      ∀ (b : ¬p i), g (Subtype.mk (p := fun (a : α) ↦ ¬p a) i b) ∈ s i
Tactic: refine forall_congr' fun i => ?_
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : α → Type u_4
p : α → Prop
inst : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x : α // p x }) → β (↑i : α)
g : (i : { x : α // ¬p x }) → β (↑i : α)
i : α
⊢ Membership.mem (α := β i) (s i)
      (((piEquivPiSubtypeProd p β).symm :
            (a : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) → (i : α) → β i)
          (f, g) i :
        β i) ↔
    (∀ (b : p i), f (Subtype.mk (p := fun (a : α) ↦ p a) i b) ∈ s i) ∧
      ∀ (b : ¬p i), g (Subtype.mk (p := fun (a : α) ↦ ¬p a) i b) ∈ s i
have pos : ∀ (hi : p i),
  Membership.mem (α := β i) (s i)
      (((piEquivPiSubtypeProd p β).symm :
            (a : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) → (i : α) → β i)
          (f, g) i :
        β i) ↔
    (∀ (b : p i), f (Subtype.mk (p := fun (a : α) ↦ p a) i b) ∈ s i) ∧
      ∀ (b : ¬p i), g (Subtype.mk (p := fun (a : α) ↦ ¬p a) i b) ∈ s i
Tactic: by_cases hi : p i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_3
β : α → Type u_4
p : α → Prop
inst : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x : α // p x }) → β (↑i : α)
g : (i : { x : α // ¬p x }) → β (↑i : α)
i : α
pos :
  ∀ (hi : p i),
    Membership.mem (α := β i) (s i)
        (((piEquivPiSubtypeProd p β).symm :
              (a : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) → (i : α) → β i)
            (f, g) i :
          β i) ↔
      (∀ (b : p i), f (Subtype.mk (p := fun (a : α) ↦ p a) i b) ∈ s i) ∧
        ∀ (b : ¬p i), g (Subtype.mk (p := fun (a : α) ↦ ¬p a) i b) ∈ s i
⊢ Membership.mem (α := β i) (s i)
      (((piEquivPiSubtypeProd p β).symm :
            (a : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) → (i : α) → β i)
          (f, g) i :
        β i) ↔
    (∀ (b : p i), f (Subtype.mk (p := fun (a : α) ↦ p a) i b) ∈ s i) ∧
      ∀ (b : ¬p i), g (Subtype.mk (p := fun (a : α) ↦ ¬p a) i b) ∈ s i
have neg : ∀ (hi : ¬p i),
  Membership.mem (α := β i) (s i)
      (((piEquivPiSubtypeProd p β).symm :
            (a : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) → (i : α) → β i)
          (f, g) i :
        β i) ↔
    (∀ (b : p i), f (Subtype.mk (p := fun (a : α) ↦ p a) i b) ∈ s i) ∧
      ∀ (b : ¬p i), g (Subtype.mk (p := fun (a : α) ↦ ¬p a) i b) ∈ s i
Tactic: by_cases hi : p i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst : EquivLike.{u_2 + 1, max 1 (u_1 + 1), u_3} E { x : α // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst_1 : DecidableEq β
inst_2 : DecidableEq α
inst_3 : (j : α) → Decidable (p j)
⊢ Eq (α := (i : α) → γ)
    (fun (i : α) ↦
      if h : p i then
        update (β := fun (a : β) ↦ γ) v j x ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h))
      else w i)
    (update (β := fun (i : α) ↦ γ)
      (fun (i : α) ↦
        if h : p i then v ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h)) else w i)
      (↑(EquivLike.inv e j) : α) x)
have h : ∀ (i : α),
  Eq.{u_4} (α := γ)
    (if h : p i then
        update (β := fun (a : β) ↦ γ) v j x ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h))
      else w i :
      γ)
    (update (β := fun (i : α) ↦ γ)
        (fun (i : α) ↦
          if h : p i then v ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h)) else w i)
        (↑(EquivLike.inv e j) : α) x i :
      γ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst : EquivLike.{u_2 + 1, max 1 (u_1 + 1), u_3} E { x : α // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst_1 : DecidableEq β
inst_2 : DecidableEq α
inst_3 : (j : α) → Decidable (p j)
i : α
⊢ Eq.{u_4} (α := γ)
    (if h : p i then
        update (β := fun (a : β) ↦ γ) v j x ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h))
      else w i :
      γ)
    (update (β := fun (i : α) ↦ γ)
        (fun (i : α) ↦
          if h : p i then v ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h)) else w i)
        (↑(EquivLike.inv e j) : α) x i :
      γ)
have pos : ∀ (h : p i),
  Eq.{u_4} (α := γ)
    (if h : p i then
        update (β := fun (a : β) ↦ γ) v j x ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h))
      else w i :
      γ)
    (update (β := fun (i : α) ↦ γ)
        (fun (i : α) ↦
          if h : p i then v ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h)) else w i)
        (↑(EquivLike.inv e j) : α) x i :
      γ)
Tactic: by_cases h : p i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst : EquivLike.{u_2 + 1, max 1 (u_1 + 1), u_3} E { x : α // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst_1 : DecidableEq β
inst_2 : DecidableEq α
inst_3 : (j : α) → Decidable (p j)
i : α
pos :
  ∀ (h : p i),
    Eq.{u_4} (α := γ)
      (if h : p i then
          update (β := fun (a : β) ↦ γ) v j x
            ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h))
        else w i :
        γ)
      (update (β := fun (i : α) ↦ γ)
          (fun (i : α) ↦
            if h : p i then v ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h)) else w i)
          (↑(EquivLike.inv e j) : α) x i :
        γ)
⊢ Eq.{u_4} (α := γ)
    (if h : p i then
        update (β := fun (a : β) ↦ γ) v j x ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h))
      else w i :
      γ)
    (update (β := fun (i : α) ↦ γ)
        (fun (i : α) ↦
          if h : p i then v ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h)) else w i)
        (↑(EquivLike.inv e j) : α) x i :
      γ)
have neg : ∀ (h : ¬p i),
  Eq.{u_4} (α := γ)
    (if h : p i then
        update (β := fun (a : β) ↦ γ) v j x ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h))
      else w i :
      γ)
    (update (β := fun (i : α) ↦ γ)
        (fun (i : α) ↦
          if h : p i then v ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h)) else w i)
        (↑(EquivLike.inv e j) : α) x i :
      γ)
Tactic: by_cases h : p i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst : EquivLike.{u_2 + 1, max 1 (u_1 + 1), u_3} E { x : α // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst_1 : DecidableEq β
inst_2 : DecidableEq α
inst_3 : (j : α) → Decidable (p j)
i : α
h : p i
⊢ Eq.{u_4} (α := γ)
    (if h : p i then
        update (β := fun (a : β) ↦ γ) v j x ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h))
      else w i :
      γ)
    (update (β := fun (i : α) ↦ γ)
        (fun (i : α) ↦
          if h : p i then v ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i h)) else w i)
        (↑(EquivLike.inv e j) : α) x i :
      γ)
have pos : (if h_1 : True then
    if (e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i sorry) = j then x
    else v ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i sorry))
  else w i) =
  if i = (↑(EquivLike.inv e j) : α) then x
  else if h_1 : True then v ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i sorry)) else w i
Tactic: simp only [h, update_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Sum (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
β : Type u_10
s : α ⊕' β
⊢ Sum.elim PSum.inl PSum.inr
      ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s inl inr : α ⊕ β)) s) =
    s
have inl : ∀ (val : α),
  Eq (α := α ⊕' β)
    (Sum.elim PSum.inl PSum.inr
      ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s inl inr : α ⊕ β)) (PSum.inl val)))
    (PSum.inl val)
Tactic: cases s
Cleared hypotheses: s