awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }
b : { y : β // y ≠ x }
a :
  (↑((fun (a : α) ↦
            (Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯ :
              { y : β // y ≠ x }))
          ((fun (b : { y : β // y ≠ x }) ↦ Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) ⋯)
            b)) :
      β) =
    (↑b : β)
⊢ (fun (a : α) ↦
        (Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯ :
          { y : β // y ≠ x }))
      ((fun (b : { y : β // y ≠ x }) ↦ Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) ⋯) b) =
    b

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }
b : { y : β // y ≠ x }
⊢ (↑((fun (a : α) ↦
            (Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯ :
              { y : β // y ≠ x }))
          ((fun (b : { y : β // y ≠ x }) ↦ Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) ⋯)
            b)) :
      β) =
    (↑b : β)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
⊢ Eq.{u_1 + 1} (α := Option α)
    ((fun (b : β) ↦
        (if h : b = x then none
          else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
          Option α))
      ((fun (a : Option α) ↦
          a.casesOn' x
            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
              (⇑e : (a : α) → { y : β // y ≠ x })))
        none))
    none

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
a : α
some : (if (↑((e : (a : α) → { y : β // y ≠ x }) a) : β) = x then none else Option.some a) = Option.some a
⊢ (fun (b : β) ↦
        (if h : b = x then none
          else Option.some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
          Option α))
      ((fun (a : Option α) ↦
          a.casesOn' x
            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
              (⇑e : (a : α) → { y : β // y ≠ x })))
        (Option.some a)) =
    Option.some a

Tactic:
simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta,
              symm_apply_apply, dite_eq_ite]

Premises used: Equiv.symm_apply_apply, Option.casesOn'_some, Subtype.coe_eta, Function.comp_apply, dite_eq_ite
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
a : α
⊢ (if (↑((e : (a : α) → { y : β // y ≠ x }) a) : β) = x then none else some a) = some a

Tactic:
if_neg (e a).property

Premises used: if_neg, DFunLike.coe, Subtype.property
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
a : α
⊢ (if (↑((e : (a : α) → { y : β // y ≠ x }) a) : β) = x then none else some a) = some a

Tactic:
exact if_neg (e a).property

Premises used: if_neg, DFunLike.coe, Subtype.property
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
a : Option α
none :
  Eq.{u_1 + 1} (α := Option α)
    ((fun (b : β) ↦
        (if h : b = x then Option.none
          else Option.some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
          Option α))
      ((fun (a : Option α) ↦
          a.casesOn' x
            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
              (⇑e : (a : α) → { y : β // y ≠ x })))
        Option.none))
    Option.none
some :
  ∀ (a : α),
    (fun (b : β) ↦
          (if h : b = x then Option.none
            else Option.some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
            Option α))
        ((fun (a : Option α) ↦
            a.casesOn' x
              (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
                (⇑e : (a : α) → { y : β // y ≠ x })))
          (Option.some a)) =
      Option.some a
⊢ (fun (b : β) ↦
        (if h : b = x then Option.none
          else Option.some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
          Option α))
      ((fun (a : Option α) ↦
          a.casesOn' x
            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
              (⇑e : (a : α) → { y : β // y ≠ x })))
        a) =
    a

Tactic:
cases a with
          | none => simp
          | some a =>
            simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta,
              symm_apply_apply, dite_eq_ite]
            exact if_neg (e a).property

Premises used: Equiv.symm_apply_apply, Option.some, Option.casesOn'_some, Option.none, Subtype.coe_eta, Function.comp_apply, dite_eq_ite
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
b : β
pos :
  ∀ (h : b = x),
    (fun (a : Option α) ↦
          a.casesOn' x
            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
              (⇑e : (a : α) → { y : β // y ≠ x })))
        ((fun (b : β) ↦
            (if h : b = x then none
              else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
              Option α))
          b) =
      b
neg :
  ∀ (h : ¬b = x),
    (fun (a : Option α) ↦
          a.casesOn' x
            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
              (⇑e : (a : α) → { y : β // y ≠ x })))
        ((fun (b : β) ↦
            (if h : b = x then none
              else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
              Option α))
          b) =
      b
⊢ (fun (a : Option α) ↦
        a.casesOn' x
          (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
            (⇑e : (a : α) → { y : β // y ≠ x })))
      ((fun (b : β) ↦
          (if h : b = x then none
            else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
            Option α))
        b) =
    b

Tactic:
by_cases h : b = x
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
b : β
h : b = x
⊢ (fun (a : Option α) ↦
        a.casesOn' x
          (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
            (⇑e : (a : α) → { y : β // y ≠ x })))
      ((fun (b : β) ↦
          (if h : b = x then none
            else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
            Option α))
        b) =
    b

Tactic:
simp [h]
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
b : β
h : ¬b = x
⊢ (fun (a : Option α) ↦
        a.casesOn' x
          (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
            (⇑e : (a : α) → { y : β // y ≠ x })))
      ((fun (b : β) ↦
          (if h : b = x then none
            else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
            Option α))
        b) =
    b

Tactic:
simp [h]
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }
⊢ Eq.{u_2 + 1} (α := β)
    (((↑((fun (e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }) ↦
                  (Subtype.mk (p := fun (e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β) ↦ (e : (a : Option α) → β) none = x)
                      {
                        toFun := fun (a : Option α) ↦
                          a.casesOn' x
                            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
                              (⇑e : (a : α) → { y : β // y ≠ x })),
                        invFun := fun (b : β) ↦
                          if h : b = x then none
                          else
                            some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)),
                        left_inv := ⋯, right_inv := ⋯ }
                      ⋯ :
                    { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }))
                ((fun (e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }) ↦
                    ({
                        toFun := fun (a : α) ↦
                          Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯,
                        invFun := fun (b : { y : β // y ≠ x }) ↦
                          Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) ⋯,
                        left_inv := ⋯, right_inv := ⋯ } :
                      Equiv.{u_1 + 1, u_2 + 1} α { y : β // y ≠ x }))
                  e)) :
            Option α ≃ β) :
          (a : Option α) → β)
        none :
      β)
    (((↑e : Option α ≃ β) : (a : Option α) → β) none : β)

Tactic:
simpa using e.property.symm

Premises used: Eq.symm, Subtype.property
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }
val : α
⊢ Eq.{u_2 + 1} (α := β)
    (((↑((fun (e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }) ↦
                  (Subtype.mk (p := fun (e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β) ↦ (e : (a : Option α) → β) none = x)
                      {
                        toFun := fun (a : Option α) ↦
                          a.casesOn' x
                            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
                              (⇑e : (a : α) → { y : β // y ≠ x })),
                        invFun := fun (b : β) ↦
                          if h : b = x then none
                          else
                            some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)),
                        left_inv := ⋯, right_inv := ⋯ }
                      ⋯ :
                    { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }))
                ((fun (e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }) ↦
                    ({
                        toFun := fun (a : α) ↦
                          Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯,
                        invFun := fun (b : { y : β // y ≠ x }) ↦
                          Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) ⋯,
                        left_inv := ⋯, right_inv := ⋯ } :
                      Equiv.{u_1 + 1, u_2 + 1} α { y : β // y ≠ x }))
                  e)) :
            Option α ≃ β) :
          (a : Option α) → β)
        (some val) :
      β)
    (((↑e : Option α ≃ β) : (a : Option α) → β) (some val) : β)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
a : α
⊢ Eq.{u_2 + 1} (α := β)
    (↑((((fun (e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }) ↦
                  ({
                      toFun := fun (a : α) ↦
                        Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯,
                      invFun := fun (b : { y : β // y ≠ x }) ↦
                        Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) ⋯,
                      left_inv := ⋯, right_inv := ⋯ } :
                    Equiv.{u_1 + 1, u_2 + 1} α { y : β // y ≠ x }))
                ((fun (e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }) ↦
                    (Subtype.mk (p := fun (e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β) ↦
                        (e : (a : Option α) → β) none = x)
                        {
                          toFun := fun (a : Option α) ↦
                            a.casesOn' x
                              (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
                                (⇑e : (a : α) → { y : β // y ≠ x })),
                          invFun := fun (b : β) ↦
                            if h : b = x then none
                            else
                              some
                                ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)),
                          left_inv := ⋯, right_inv := ⋯ }
                        ⋯ :
                      { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }))
                  e) :
              Equiv.{u_1 + 1, u_2 + 1} α { y : β // y ≠ x }) :
            (a : α) → { y : β // y ≠ x })
          a) :
      β)
    (↑((e : (a : α) → { y : β // y ≠ x }) a) : β)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
x : β
e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }
a : α
h : ((↑e : Option α ≃ β) : (a : Option α) → β) (some a) ≠ x
⊢ Eq.{u_2 + 1} (α := { y : β // y ≠ x })
    ((((optionSubtype x : (a : { e : Option α ≃ β // (e : (a : Option α) → β) none = x }) → α ≃ { y : β // y ≠ x }) e :
            Equiv.{u_1 + 1, u_2 + 1} α { y : β // y ≠ x }) :
          (a : α) → { y : β // y ≠ x })
        a :
      { y : β // y ≠ x })
    (Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) h : { y : β // y ≠ x })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
x : β
e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }
a : α
⊢ Eq.{u_2 + 1} (α := β)
    ((↑((((optionSubtype x : (a : { e : Option α ≃ β // (e : (a : Option α) → β) none = x }) → α ≃ { y : β // y ≠ x })
                  e :
                Equiv.{u_1 + 1, u_2 + 1} α { y : β // y ≠ x }) :
              (a : α) → { y : β // y ≠ x })
            a) :
        β) :
      β)
    (((↑e : Option α ≃ β) : (a : Option α) → β) (some a) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
x : β
e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }
b : { y : β // y ≠ x }
dsimp :
  Eq.{u_1 + 1} (α := Option α)
    (some
        ((Equiv.symm
              (({
                    toFun :=
                      fun (e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }) ↦
                      {
                        toFun := fun (a : α) ↦
                          Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯,
                        invFun := fun (b : { y : β // y ≠ x }) ↦
                          Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) ⋯,
                        left_inv := ⋯, right_inv := ⋯ },
                    invFun := fun (e : Equiv.{u_1 + 1, u_2 + 1} α { y : β // y ≠ x }) ↦
                      Subtype.mk (p := fun (e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β) ↦
                        (e : (a : Option α) → β) none = x)
                        {
                          toFun := fun (a : Option α) ↦
                            a.casesOn' x
                              (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
                                (⇑e : (a : α) → { y : β // y ≠ x })),
                          invFun := fun (b : β) ↦
                            if h : b = x then none
                            else
                              some
                                ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)),
                          left_inv := ⋯, right_inv := ⋯ }
                        ⋯,
                    left_inv := ⋯, right_inv := ⋯ } :
                  (a : { e : Option α ≃ β // (e : (a : Option α) → β) none = x }) → α ≃ { y : β // y ≠ x })
                e) :
            (a : { y : β // y ≠ x }) → α)
          b) :
      Option α)
    (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β) : Option α)
⊢ Eq.{u_1 + 1} (α := Option α)
    (some
        ((Equiv.symm
              ((optionSubtype x :
                  (a : { e : Option α ≃ β // (e : (a : Option α) → β) none = x }) → α ≃ { y : β // y ≠ x })
                e) :
            (a : { y : β // y ≠ x }) → α)
          b) :
      Option α)
    (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β) : Option α)

Tactic:
dsimp only [optionSubtype]

Premises used: Equiv.optionSubtype
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
x : β
e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }
b : { y : β // y ≠ x }
⊢ Eq.{u_1 + 1} (α := Option α)
    (some
        ((Equiv.symm
              (({
                    toFun :=
                      fun (e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }) ↦
                      {
                        toFun := fun (a : α) ↦
                          Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯,
                        invFun := fun (b : { y : β // y ≠ x }) ↦
                          Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) ⋯,
                        left_inv := ⋯, right_inv := ⋯ },
                    invFun := fun (e : Equiv.{u_1 + 1, u_2 + 1} α { y : β // y ≠ x }) ↦
                      Subtype.mk (p := fun (e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β) ↦
                        (e : (a : Option α) → β) none = x)
                        {
                          toFun := fun (a : Option α) ↦
                            a.casesOn' x
                              (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
                                (⇑e : (a : α) → { y : β // y ≠ x })),
                          invFun := fun (b : β) ↦
                            if h : b = x then none
                            else
                              some
                                ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)),
                          left_inv := ⋯, right_inv := ⋯ }
                        ⋯,
                    left_inv := ⋯, right_inv := ⋯ } :
                  (a : { e : Option α ≃ β // (e : (a : Option α) → β) none = x }) → α ≃ { y : β // y ≠ x })
                e) :
            (a : { y : β // y ≠ x }) → α)
          b) :
      Option α)
    (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β) : Option α)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
a : α
⊢ Eq.{u_2 + 1} (α := β)
    (((↑((Equiv.symm (optionSubtype x) :
                  (a : α ≃ { y : β // y ≠ x }) → { e : Option α ≃ β // (e : (a : Option α) → β) none = x })
                e) :
            Option α ≃ β) :
          (a : Option α) → β)
        (some a) :
      β)
    ((↑((e : (a : α) → { y : β // y ≠ x }) a) : β) : β)

Tactic:
rfl

Premises used: Option.casesOn', rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
⊢ ((↑((Equiv.symm (optionSubtype x) :
                (a : α ≃ { y : β // y ≠ x }) → { e : Option α ≃ β // (e : (a : Option α) → β) none = x })
              e) :
          Option α ≃ β) :
        (a : Option α) → β)
      none =
    x

Tactic:
rfl

Premises used: Option.casesOn', rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
b : { y : β // y ≠ x }
simp :
  (↑b : β) = x →
    Eq.{u_1 + 1} (α := Option α) (none : Option α) (some ((e.symm : (a : { y : β // y ≠ x }) → α) b) : Option α)
⊢ Eq.{u_1 + 1} (α := Option α)
    ((Equiv.symm
            (↑((Equiv.symm (optionSubtype x) :
                    (a : α ≃ { y : β // y ≠ x }) → { e : Option α ≃ β // (e : (a : Option α) → β) none = x })
                  e) :
              Option α ≃ β) :
          (a : β) → Option α)
        (↑b : β) :
      Option α)
    (some ((e.symm : (a : { y : β // y ≠ x }) → α) b) : Option α)

Tactic:
simp only [optionSubtype, coe_fn_symm_mk, Subtype.coe_mk,
             Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]

Premises used: Subtype.coe_mk, Equiv.coe_fn_symm_mk, ite_eq_right_iff, Subtype.coe_eta, dite_eq_ite, Equiv.optionSubtype
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
b : { y : β // y ≠ x }
⊢ (↑b : β) = x →
    Eq.{u_1 + 1} (α := Option α) (none : Option α) (some ((e.symm : (a : { y : β // y ≠ x }) → α) b) : Option α)

Tactic:
fun h => False.elim (b.property h)

Premises used: False.elim, Subtype.property
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
b : { y : β // y ≠ x }
⊢ (↑b : β) = x →
    Eq.{u_1 + 1} (α := Option α) (none : Option α) (some ((e.symm : (a : { y : β // y ≠ x }) → α) b) : Option α)

Tactic:
exact fun h => False.elim (b.property h)

Premises used: False.elim, Subtype.property
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ Eq (α := Option { b : α // b ≠ a })
    (((optionSubtypeNe a).symm : (a_1 : α) → Option { b : α // b ≠ a }) a : Option { b : α // b ≠ a })
    (none : Option { b : α // b ≠ a })

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
inst : DecidableEq α
a b : α
hba : b ≠ a
⊢ Eq (α := Option { b : α // b ≠ a })
    (((optionSubtypeNe a).symm : (a_1 : α) → Option { b : α // b ≠ a }) b : Option { b : α // b ≠ a })
    (some (Subtype.mk (p := fun (b : α) ↦ b ≠ a) b hba) : Option { b : α // b ≠ a })

Tactic:
simp [hba]
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ (optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) none = a

Tactic:
rfl

Premises used: Option.casesOn', rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
inst : DecidableEq α
a : α
b : { b : α // b ≠ a }
⊢ (optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) (some b) = (↑b : α)

Tactic:
rfl

Premises used: Option.casesOn', rfl