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
β_2 : Type u_2
α : Type u_3
β : Type u_4
val : α
x : β
h' : Sum.inr x = Sum.inl val
⊢ False

Tactic:
cases h'
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
x : β
⊢ (rangeInr α β : (a : (↑(range Sum.inr) : Type (max u_3 u_4))) → β)
      (Subtype.mk (p := fun (x : α ⊕ β) ↦ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) x) (Sum.inr x) ⋯) =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Sort u_3
β : Type u_4
f : α → β
hf : Injective f
b : (↑(range f) : Type u_4)
⊢ f (((ofInjective f hf).symm : (a : (↑(range f) : Type u_4)) → α) b) = (↑b : β)

Tactic:
Subtype.ext_iff.1 <| (ofInjective f hf).apply_symm_apply b

Premises used: Equiv.apply_symm_apply, Subtype.ext_iff, Equiv.ofInjective, Iff.mp
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Sort u_3
β : Type u_4
f : α → β
hf : Injective f
a : α
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) ⋯)) :
      (↑(range f) : Type u_4))
    ((ofInjective f hf : (a : α) → (↑(range f) : Type u_4)) 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) ⋯) =
    a

Tactic:
apply (ofInjective f hf).injective

Premises used: Equiv.ofInjective, Equiv.injective
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Sort u_3
β : Type u_4
f : α → β
hf : Injective f
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) ⋯)) :
      (↑(range f) : Type u_4))
    ((ofInjective f hf : (a : α) → (↑(range f) : Type u_4)) a : (↑(range f) : Type u_4))

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
h :
  ∀ (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) ⋯)
⊢ (⇑(ofInjective f hf).symm : (a : (↑(range f) : Type u_4)) → α) = rangeSplitting f

Tactic:
ext ⟨y, x, rfl⟩

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
x : α
h :
  f
      (((ofInjective f hf).symm : (a : (↑(range f) : Type u_4)) → α)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) ⋯)) =
    f (rangeSplitting f (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (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) ⋯)

Tactic:
apply hf
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
x : α
⊢ f
      (((ofInjective f hf).symm : (a : (↑(range f) : Type u_4)) → α)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) ⋯)) =
    f (rangeSplitting f (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) ⋯))

Tactic:
simp [apply_rangeSplitting f]

Premises used: Set.apply_rangeSplitting
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Sort u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ Eq (α := (↑(range f) : Type u_4) → β) (f ∘ (⇑(ofInjective f hf).symm : (a : (↑(range f) : Type u_4)) → α))
    (Subtype.val (p := fun (x : β) ↦ x ∈ range f))

Tactic:
funext fun x => apply_ofInjective_symm hf x

Premises used: funext, Equiv.apply_ofInjective_symm
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
H :
  ∀ (x : α),
    Eq.{u_4 + 1} (α := β) (↑((ofLeftInverse f f_inv hf : (a : α) → (↑(range f) : Type u_4)) x) : β)
      (↑((ofInjective f ⋯ : (a : α) → (↑(range f) : Type u_4)) x) : β)
⊢ ofLeftInverse f f_inv hf = ofInjective f ⋯

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
x : α
⊢ Eq.{u_4 + 1} (α := β) (↑((ofLeftInverse f f_inv hf : (a : α) → (↑(range f) : Type u_4)) x) : β)
    (↑((ofInjective f ⋯ : (a : α) → (↑(range f) : Type u_4)) x) : β)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
H :
  ∀ (x : α),
    Eq.{u_4 + 1} (α := β) (↑((ofLeftInverse' f f_inv hf : (a : α) → (↑(range f) : Type u_4)) x) : β)
      (↑((ofInjective f ⋯ : (a : α) → (↑(range f) : Type u_4)) x) : β)
⊢ ofLeftInverse' f f_inv hf = ofInjective f ⋯

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
x : α
⊢ Eq.{u_4 + 1} (α := β) (↑((ofLeftInverse' f f_inv hf : (a : α) → (↑(range f) : Type u_4)) x) : β)
    (↑((ofInjective f ⋯ : (a : α) → (↑(range f) : Type u_4)) x) : β)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
p : Set α → Prop
⊢ (∀ (a : Set α), p a) ↔ ∀ (a : Set β), p ((⇑e : (a : α) → β) ⁻¹' a)

Tactic:
e.injective.preimage_surjective.forall

Premises used: Function.Injective.preimage_surjective, Function.Surjective.forall, Equiv.injective
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : α → Type u_4
p : α → Prop
inst : DecidablePred p
s : (i : α) → Set (β i)
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 : α))
⊢ (⇑(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 : α))

Tactic:
ext ⟨f, g⟩
-- Module: Mathlib.Logic.Equiv.Set
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 : α)
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
⊢ 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:
simp only [mem_preimage, mem_univ_pi, prodMk_mem_set_prod_eq, Subtype.forall, ← forall_and]

Premises used: Subtype.forall, Set.prodMk_mem_set_prod_eq, Set.mem_univ_pi, Set.mem_preimage, forall_and
-- Module: Mathlib.Logic.Equiv.Set
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

Tactic:
forall_congr' fun i => ?_

Premises used: forall_congr'
-- Module: Mathlib.Logic.Equiv.Set
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 : α)
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
⊢ (∀ (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:
refine forall_congr' fun i => ?_

Premises used: forall_congr'
-- Module: Mathlib.Logic.Equiv.Set
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
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
⊢ 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
-- Module: Mathlib.Logic.Equiv.Set
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 : α
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:
simp [hi]
-- Module: Mathlib.Logic.Equiv.Set
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 : α
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:
simp [hi]
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → γ
g : β → γ
e : (c : γ) → Equiv.{u_3 + 1, u_4 + 1} (↑(f ⁻¹' {c}) : Type u_3) (↑(g ⁻¹' {c}) : Type u_4)
a : α
⊢ g ((ofPreimageEquiv e : (a : α) → β) a) = f a

Tactic:
Equiv.ofFiberEquiv_map e a

Premises used: Equiv.ofFiberEquiv_map
-- Module: Mathlib.Logic.Equiv.Set
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)
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 :
        γ)
⊢ 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)

Tactic:
ext i
-- Module: Mathlib.Logic.Equiv.Set
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 :
        γ)
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 :
        γ)
⊢ 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
-- Module: Mathlib.Logic.Equiv.Set
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
pos :
  (if h_1 : True then
      if (e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i ⋯) = j then x
      else v ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i ⋯))
    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 ⋯)) else w 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:
simp only [h, update_apply]

Premises used: Function.update_apply
-- Module: Mathlib.Logic.Equiv.Set
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
⊢ (if h_1 : True then
      if (e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i ⋯) = j then x
      else v ((e : (a : { x : α // p x }) → β) (Subtype.mk (p := fun (x : α) ↦ p x) i ⋯))
    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 ⋯)) else w i

Tactic:
aesop
-- Module: Mathlib.Logic.Equiv.Set
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 :
      γ)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
⊢ BijOn (⇑(swap a b) : (a : α) → α) s s

Tactic:
grind [Equiv.bijOn]

Premises used: Equiv.bijOn
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : ¬b ∈ s
⊢ BijOn (⇑(swap a b) : (a : α) → α) s (insert b (s \ {a}))

Tactic:
grind [Equiv.bijOn]

Premises used: Equiv.bijOn
-- Module: Mathlib.Logic.Equiv.Sum
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 : α ⊕' β
inl :
  ∀ (val : α),
    Eq (α := α ⊕' β)
      (Sum.elim PSum.inl PSum.inr
        ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s Sum.inl Sum.inr : α ⊕ β))
          (PSum.inl val)))
      (PSum.inl val)
inr :
  ∀ (val : β),
    Eq (α := α ⊕' β)
      (Sum.elim PSum.inl PSum.inr
        ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s Sum.inl Sum.inr : α ⊕ β))
          (PSum.inr val)))
      (PSum.inr val)
⊢ Sum.elim PSum.inl PSum.inr
      ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s Sum.inl Sum.inr : α ⊕ β)) s) =
    s

Tactic:
cases s
-- Module: Mathlib.Logic.Equiv.Sum
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
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:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
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
val : β
⊢ Eq (α := α ⊕' β)
    (Sum.elim PSum.inl PSum.inr
      ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s inl inr : α ⊕ β)) (PSum.inr val)))
    (PSum.inr val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
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 : α ⊕ β
inl :
  ∀ (val : α),
    Eq (α := α ⊕ β)
      ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s Sum.inl Sum.inr : α ⊕ β))
        (Sum.elim PSum.inl PSum.inr (Sum.inl val)))
      (Sum.inl val)
inr :
  ∀ (val : β),
    Eq (α := α ⊕ β)
      ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s Sum.inl Sum.inr : α ⊕ β))
        (Sum.elim PSum.inl PSum.inr (Sum.inr val)))
      (Sum.inr val)
⊢ (fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s Sum.inl Sum.inr : α ⊕ β))
      (Sum.elim PSum.inl PSum.inr s) =
    s

Tactic:
cases s
-- Module: Mathlib.Logic.Equiv.Sum
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
val : α
⊢ Eq (α := α ⊕ β)
    ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s inl inr : α ⊕ β))
      (Sum.elim PSum.inl PSum.inr (inl val)))
    (inl val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
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
val : β
⊢ Eq (α := α ⊕ β)
    ((fun (s : α ⊕' β) ↦ (PSum.casesOn (motive := fun (x : α ⊕' β) ↦ α ⊕ β) s inl inr : α ⊕ β))
      (Sum.elim PSum.inl PSum.inr (inr val)))
    (inr val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Sort u_1
α₁_1 : Sort u_2
α₂_1 : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂_1 : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
x : α₁ ⊕ β₁
⊢ Sum.map.{u_10, u_9, u_12, u_11} (α := α₂) (β := β₂) (⇑ea.symm : (a : α₂) → α₁) (⇑eb.symm : (a : β₂) → β₁)
      (Sum.map (⇑ea : (a : α₁) → α₂) (⇑eb : (a : β₁) → β₂) x) =
    x

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Sort u_1
α₁_1 : Sort u_2
α₂_1 : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂_1 : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
x : α₂ ⊕ β₂
⊢ Sum.map.{u_9, u_10, u_11, u_12} (α := α₁) (β := β₁) (⇑ea : (a : α₁) → α₂) (⇑eb : (a : β₁) → β₂)
      (Sum.map (⇑ea.symm : (a : α₂) → α₁) (⇑eb.symm : (a : β₂) → β₁) x) =
    x

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
H :
  ∀ (i : α₁ ⊕ α₂),
    Eq (α := γ₁ ⊕ γ₂) (((e.sumCongr f).trans (g.sumCongr h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) i : γ₁ ⊕ γ₂)
      (((e.trans g).sumCongr (f.trans h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) i : γ₁ ⊕ γ₂)
⊢ (e.sumCongr f).trans (g.sumCongr h) = (e.trans g).sumCongr (f.trans h)

Tactic:
ext i
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
i : α₁ ⊕ α₂
H :
  ∀ (val : α₁),
    Eq (α := γ₁ ⊕ γ₂) (((e.sumCongr f).trans (g.sumCongr h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inl val) : γ₁ ⊕ γ₂)
      (((e.trans g).sumCongr (f.trans h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inl val) : γ₁ ⊕ γ₂)
H₁ :
  ∀ (val : α₂),
    Eq (α := γ₁ ⊕ γ₂) (((e.sumCongr f).trans (g.sumCongr h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inr val) : γ₁ ⊕ γ₂)
      (((e.trans g).sumCongr (f.trans h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) (inr val) : γ₁ ⊕ γ₂)
⊢ Eq (α := γ₁ ⊕ γ₂) (((e.sumCongr f).trans (g.sumCongr h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) i : γ₁ ⊕ γ₂)
    (((e.trans g).sumCongr (f.trans h) : (a : α₁ ⊕ α₂) → γ₁ ⊕ γ₂) i : γ₁ ⊕ γ₂)

Tactic:
cases i