awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Nat
Goal:
h :
  ∀ (x : ℕ),
    Eq (α := ℕ) ((natSumNatEquivNat : (a : ℕ ⊕ ℕ) → ℕ) (Sum.inl x) : ℕ)
      (Sum.elim (fun (x : ℕ) ↦ 2 * x) (fun (x : ℕ) ↦ 2 * x + 1) (Sum.inl x) : ℕ)
h₁ :
  ∀ (x : ℕ),
    Eq (α := ℕ) ((natSumNatEquivNat : (a : ℕ ⊕ ℕ) → ℕ) (Sum.inr x) : ℕ)
      (Sum.elim (fun (x : ℕ) ↦ 2 * x) (fun (x : ℕ) ↦ 2 * x + 1) (Sum.inr x) : ℕ)
⊢ Eq (α := (a : ℕ ⊕ ℕ) → ℕ) (⇑natSumNatEquivNat : (a : ℕ ⊕ ℕ) → ℕ)
    (Sum.elim (fun (x : ℕ) ↦ 2 * x) fun (x : ℕ) ↦ 2 * x + 1)

Tactic:
ext (x | x)
-- Module: Mathlib.Logic.Equiv.Nat
Goal:
x : ℕ
⊢ Eq (α := ℕ) ((natSumNatEquivNat : (a : ℕ ⊕ ℕ) → ℕ) (Sum.inl x) : ℕ)
    (Sum.elim (fun (x : ℕ) ↦ 2 * x) (fun (x : ℕ) ↦ 2 * x + 1) (Sum.inl x) : ℕ)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Nat
Goal:
x : ℕ
⊢ Eq (α := ℕ) ((natSumNatEquivNat : (a : ℕ ⊕ ℕ) → ℕ) (Sum.inr x) : ℕ)
    (Sum.elim (fun (x : ℕ) ↦ 2 * x) (fun (x : ℕ) ↦ 2 * x + 1) (Sum.inr x) : ℕ)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
⊢ (Equiv.refl α).optionCongr = Equiv.refl (Option α)

Tactic:
ext <| congr_fun Option.map_id

Premises used: Equiv.ext, congr_fun, Option.map_id
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
⊢ e.symm.optionCongr = e.optionCongr.symm

Tactic:
rfl

Premises used: Equiv.symm, Equiv.optionCongr, rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
H :
  ∀ (x : Option α),
    Eq.{u_3 + 1} (α := Option γ) (((e₁.trans e₂).optionCongr : (a : Option α) → Option γ) x : Option γ)
      ((e₁.optionCongr.trans e₂.optionCongr : (a : Option α) → Option γ) x : Option γ)
⊢ (e₁.trans e₂).optionCongr = e₁.optionCongr.trans e₂.optionCongr

Tactic:
ext x : 1
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
x : Option α
H :
  Eq.{u_3 + 1} (α := Option γ) ((e₁.optionCongr.trans e₂.optionCongr : (a : Option α) → Option γ) x : Option γ)
    (((e₁.trans e₂).optionCongr : (a : Option α) → Option γ) x : Option γ)
⊢ Eq.{u_3 + 1} (α := Option γ) (((e₁.trans e₂).optionCongr : (a : Option α) → Option γ) x : Option γ)
    ((e₁.optionCongr.trans e₂.optionCongr : (a : Option α) → Option γ) x : Option γ)

Tactic:
symm
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
x : Option α
⊢ Eq.{u_3 + 1} (α := Option γ) ((e₁.optionCongr.trans e₂.optionCongr : (a : Option α) → Option γ) x : Option γ)
    (((e₁.trans e₂).optionCongr : (a : Option α) → Option γ) x : Option γ)

Tactic:
apply Option.map_map

Premises used: Option.map_map
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α β : Type u
e : α ≃ β
⊢ e.optionCongr = EquivFunctor.mapEquiv Option e

Tactic:
rfl

Premises used: EquivFunctor.mapEquiv, rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h : ¬isSome.{u_2} (α := β) ((e : (a : Option α) → Option β) (some x)) = true
rw : Ne.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) none : Option β) (none : Option β)
⊢ isSome.{u_2} (α := β) ((e : (a : Option α) → Option β) none) = true

Tactic:
rw [← Option.ne_none_iff_isSome]

Premises used: Option.ne_none_iff_isSome
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h : ¬isSome.{u_2} (α := β) ((e : (a : Option α) → Option β) (some x)) = true
hn : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) none : Option β) (none : Option β)
⊢ Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β)
    ((e : (a : Option α) → Option β) none : Option β)

Tactic:
rw [Option.not_isSome_iff_eq_none, ← hn] at h

Premises used: Option.not_isSome_iff_eq_none
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h : ¬isSome.{u_2} (α := β) ((e : (a : Option α) → Option β) (some x)) = true
hn : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) none : Option β) (none : Option β)
h₁ :
  Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β)
    ((e : (a : Option α) → Option β) none : Option β)
⊢ Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) none : Option β) (none : Option β)

Tactic:
rw [Option.not_isSome_iff_eq_none, ← hn] at h

Premises used: Option.not_isSome_iff_eq_none
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h :
  Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β)
    ((e : (a : Option α) → Option β) none : Option β)
hn : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) none : Option β) (none : Option β)
⊢ False

Tactic:
Option.some_ne_none _ (e.injective h)

Premises used: Equiv.injective, Option.some_ne_none
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h :
  Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β)
    ((e : (a : Option α) → Option β) none : Option β)
hn : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) none : Option β) (none : Option β)
⊢ False

Tactic:
exact Option.some_ne_none _ (e.injective h)

Premises used: Equiv.injective, Option.some_ne_none
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h : ∃ (x' : β), (e : (a : Option α) → Option β) (some x) = some x'
⊢ some (e.removeNone_aux x) = (e : (a : Option α) → Option β) (some x)

Tactic:
simp [removeNone_aux, Option.isSome_iff_exists.mpr h]

Premises used: Iff.mpr, Equiv.removeNone_aux, Option.isSome_iff_exists
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)
⊢ some (e.removeNone_aux x) = (e : (a : Option α) → Option β) none

Tactic:
simp [removeNone_aux, Option.not_isSome_iff_eq_none.mpr h]

Premises used: Iff.mpr, Equiv.removeNone_aux, Option.not_isSome_iff_eq_none
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
none :
  ∀
    (h1 :
      Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) (Option.some (e.removeNone_aux x)) : Option α)
        (Option.none : Option α)),
    Option.some (e.symm.removeNone_aux (e.removeNone_aux x)) = Option.some x
some :
  ∀ (val : α) (h1 : (e.symm : (a : Option β) → Option α) (Option.some (e.removeNone_aux x)) = Option.some val),
    Option.some (e.symm.removeNone_aux (e.removeNone_aux x)) = Option.some x
⊢ Option.some (e.symm.removeNone_aux (e.removeNone_aux x)) = Option.some x

Tactic:
cases h1 : e.symm (some (removeNone_aux e x))

Premises used: Equiv.removeNone_aux, Option.some, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h1 :
  Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) : Option α)
    (Option.none : Option α)
none :
  ∀ (h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (Option.none : Option β)),
    some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
none₁ :
  ∀ (val : β) (h2 : (e : (a : Option α) → Option β) (some x) = some val),
    some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Tactic:
cases h2 : e (some x)

Premises used: Option.some, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x val : α
h1 : (e.symm : (a : Option β) → Option α) (Option.some (e.removeNone_aux x)) = Option.some val
some :
  ∀ (h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (Option.some x) : Option β) (none : Option β)),
    Option.some (e.symm.removeNone_aux (e.removeNone_aux x)) = Option.some x
some₁ :
  ∀ (val : β) (h2 : (e : (a : Option α) → Option β) (Option.some x) = Option.some val),
    Option.some (e.symm.removeNone_aux (e.removeNone_aux x)) = Option.some x
⊢ Option.some (e.symm.removeNone_aux (e.removeNone_aux x)) = Option.some x

Tactic:
cases h2 : e (some x)

Premises used: Option.some, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h1 :
  Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) : Option α)
    (Option.none : Option α)
h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (Option.none : Option β)
none : (e.symm : (a : Option β) → Option α) Option.none = some x
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Tactic:
rw [removeNone_aux_none _ h1]

Premises used: Equiv.removeNone_aux_none
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h1 :
  Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) : Option α)
    (none : Option α)
h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)
⊢ (e.symm : (a : Option β) → Option α) none = some x

Tactic:
(e.eq_symm_apply.mpr h2).symm

Premises used: Iff.mpr, Eq.symm, Equiv.eq_symm_apply
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h1 :
  Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) : Option α)
    (none : Option α)
h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)
⊢ (e.symm : (a : Option β) → Option α) none = some x

Tactic:
exact (e.eq_symm_apply.mpr h2).symm

Premises used: Iff.mpr, Eq.symm, Equiv.eq_symm_apply
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h1 :
  Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) : Option α)
    (Option.none : Option α)
val : β
h2 : (e : (a : Option α) → Option β) (some x) = some val
none :
  ∀
    (h1 :
      Eq.{u_1 + 1} (α := Option α)
        ((e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) (some x)) : Option α)
        (Option.none : Option α))
    (val : β) (h2 : (e : (a : Option α) → Option β) (some x) = some val),
    some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Tactic:
rw [removeNone_aux_some _ ⟨_, h2⟩] at h1

Premises used: Exists.intro, Equiv.removeNone_aux_some
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h1 :
  Eq.{u_1 + 1} (α := Option α)
    ((e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) (some x)) : Option α) (none : Option α)
val : β
h2 : (e : (a : Option α) → Option β) (some x) = some val
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Tactic:
simp at h1
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x val : α
h1 : (e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) = some val
h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)
⊢ (e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) none) = some val

Tactic:
rw [removeNone_aux_none _ h2] at h1

Premises used: Equiv.removeNone_aux_none
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x val : α
h1 : (e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) = some val
h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)
h1₁ : (e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) none) = some val
⊢ Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)

Tactic:
rw [removeNone_aux_none _ h2] at h1

Premises used: Equiv.removeNone_aux_none
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x val : α
h1 : (e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) none) = some val
h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x

Tactic:
simp at h1
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x val : α
h1 : (e.symm : (a : Option β) → Option α) (Option.some (e.removeNone_aux x)) = Option.some val
val_1 : β
h2 : (e : (a : Option α) → Option β) (Option.some x) = Option.some val_1
some : (e.symm : (a : Option β) → Option α) (Option.some (e.removeNone_aux x)) = Option.some x
⊢ Option.some (e.symm.removeNone_aux (e.removeNone_aux x)) = Option.some x

Tactic:
rw [removeNone_aux_some _ ⟨_, h1⟩]

Premises used: Exists.intro, Equiv.removeNone_aux_some
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x val : α
h1 : (e.symm : (a : Option β) → Option α) (Option.some (e.removeNone_aux x)) = Option.some val
val_1 : β
h2 : (e : (a : Option α) → Option β) (Option.some x) = Option.some val_1
some : (e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) (Option.some x)) = Option.some x
⊢ (e.symm : (a : Option β) → Option α) (Option.some (e.removeNone_aux x)) = Option.some x

Tactic:
rw [removeNone_aux_some _ ⟨_, h2⟩]

Premises used: Exists.intro, Equiv.removeNone_aux_some
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x val : α
h1 : (e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) = some val
val_1 : β
h2 : (e : (a : Option α) → Option β) (some x) = some val_1
⊢ (e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) (some x)) = some x

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
⊢ e.removeNone.symm = e.symm.removeNone

Tactic:
rfl

Premises used: Equiv.removeNone_aux, dite, Equiv.removeNone, Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h : ∃ (x' : β), (e : (a : Option α) → Option β) (some x) = some x'
⊢ Eq.{u_2 + 1} (α := Option β) (some ((e.removeNone : (a : α) → β) x) : Option β)
    ((e : (a : Option α) → Option β) (some x) : Option β)

Tactic:
removeNone_aux_some e h

Premises used: Equiv.removeNone_aux, dite, Equiv.removeNone_aux_some
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)
⊢ Eq.{u_2 + 1} (α := Option β) (some ((e.removeNone : (a : α) → β) x) : Option β)
    ((e : (a : Option α) → Option β) none : Option β)

Tactic:
removeNone_aux_none e h

Premises used: Equiv.removeNone_aux, dite, Equiv.removeNone_aux_none
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
h : Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) none : Option α) (none : Option α)
⊢ Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) none : Option β) (none : Option β)

Tactic:
simpa using (congr_arg e h).symm

Premises used: congr_arg, Eq.symm, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
h : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) none : Option β) (none : Option β)
⊢ Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) none : Option α) (none : Option α)

Tactic:
simpa using (congr_arg e.symm h).symm

Premises used: congr_arg, Equiv.symm, Eq.symm, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
none :
  ∀
    (h :
      Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (Option.some x) : Option β)
        (Option.none : Option β)),
    Eq.{u_2 + 1} (α := Option β) (Option.some ((e.removeNone : (a : α) → β) x) : Option β)
        ((e : (a : Option α) → Option β) Option.none : Option β) ↔
      (e.symm : (a : Option β) → Option α) Option.none = Option.some x
some :
  ∀ (a : β) (h : (e : (a : Option α) → Option β) (Option.some x) = Option.some a),
    Eq.{u_2 + 1} (α := Option β) (Option.some ((e.removeNone : (a : α) → β) x) : Option β)
        ((e : (a : Option α) → Option β) Option.none : Option β) ↔
      (e.symm : (a : Option β) → Option α) Option.none = Option.some x
⊢ Eq.{u_2 + 1} (α := Option β) (Option.some ((e.removeNone : (a : α) → β) x) : Option β)
      ((e : (a : Option α) → Option β) Option.none : Option β) ↔
    (e.symm : (a : Option β) → Option α) Option.none = Option.some x

Tactic:
rcases h : e (some x) with a | a

Premises used: Option.some, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (Option.none : Option β)
none :
  Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) Option.none : Option β)
      ((e : (a : Option α) → Option β) Option.none : Option β) ↔
    (e.symm : (a : Option β) → Option α) Option.none = some x
⊢ Eq.{u_2 + 1} (α := Option β) (some ((e.removeNone : (a : α) → β) x) : Option β)
      ((e : (a : Option α) → Option β) Option.none : Option β) ↔
    (e.symm : (a : Option β) → Option α) Option.none = some x

Tactic:
rw [removeNone_none _ h]

Premises used: Equiv.removeNone_none
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)
⊢ Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) none : Option β)
      ((e : (a : Option α) → Option β) none : Option β) ↔
    (e.symm : (a : Option β) → Option α) none = some x

Tactic:
simpa using (congr_arg e.symm h).symm

Premises used: congr_arg, Equiv.symm, Eq.symm, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
a : β
h : (e : (a : Option α) → Option β) (Option.some x) = Option.some a
some :
  Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (Option.some x) : Option β)
      ((e : (a : Option α) → Option β) none : Option β) ↔
    (e.symm : (a : Option β) → Option α) none = Option.some x
⊢ Eq.{u_2 + 1} (α := Option β) (Option.some ((e.removeNone : (a : α) → β) x) : Option β)
      ((e : (a : Option α) → Option β) none : Option β) ↔
    (e.symm : (a : Option β) → Option α) none = Option.some x

Tactic:
rw [removeNone_some _ ⟨a, h⟩]

Premises used: Exists.intro, Equiv.removeNone_some
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
a : β
h : (e : (a : Option α) → Option β) (some x) = some a
⊢ Eq.{u_1 + 1} (α := Option α)
    ((e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) (some x)) : Option α)
    ((e.symm : (a : Option β) → Option α) (some a) : Option α)

Tactic:
have h1 := congr_arg e.symm h
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
a : β
h : (e : (a : Option α) → Option β) (some x) = some a
h1 :
  Eq.{u_1 + 1} (α := Option α)
    ((e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) (some x)) : Option α)
    ((e.symm : (a : Option β) → Option α) (some a) : Option α)
⊢ some x = (e.symm : (a : Option β) → Option α) (some a)

Tactic:
rw [symm_apply_apply] at h1

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
a : β
h : (e : (a : Option α) → Option β) (Option.some x) = Option.some a
h1 : Option.some x = (e.symm : (a : Option β) → Option α) (Option.some a)
some : False ↔ (e.symm : (a : Option β) → Option α) none = Option.some x
⊢ Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (Option.some x) : Option β)
      ((e : (a : Option α) → Option β) none : Option β) ↔
    (e.symm : (a : Option β) → Option α) none = Option.some x

Tactic:
simp only [apply_eq_iff_eq, reduceCtorEq]

Premises used: reduceCtorEq, Equiv.apply_eq_iff_eq
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
a : β
h : (e : (a : Option α) → Option β) (some x) = some a
h1 : some x = (e.symm : (a : Option β) → Option α) (some a)
⊢ False ↔ (e.symm : (a : Option β) → Option α) none = some x

Tactic:
simp [h1]
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
x : α
⊢ Eq.{u_2 + 1} (α := Option β) ((e.optionCongr : (a : Option α) → Option β) (some x) : Option β)
    (some ((e : (a : α) → β) x) : Option β)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_1
β : Type u_2
⊢ Function.Injective (α := α ≃ β) optionCongr

Tactic:
Function.LeftInverse.injective removeNone_optionCongr

Premises used: Function.LeftInverse.injective, Equiv.removeNone_optionCongr
-- 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 }
a : α
rw :
  ((↑e : Option α ≃ β).symm : (a : β) → Option α)
      (↑((fun (a : α) ↦
              (Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯ :
                { y : β // y ≠ x }))
            a) :
        β) =
    some a
⊢ (fun (b : { y : β // y ≠ x }) ↦ Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) ⋯)
      ((fun (a : α) ↦
          (Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯ :
            { y : β // y ≠ x }))
        a) =
    a

Tactic:
rw [← some_inj, some_get]

Premises used: Option.some_get, Option.some_inj
-- 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 }
a : α
⊢ ((↑e : Option α ≃ β).symm : (a : β) → Option α)
      (↑((fun (a : α) ↦
              (Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯ :
                { y : β // y ≠ x }))
            a) :
        β) =
    some a

Tactic:
symm_apply_apply (e : Option α ≃ β) a

Premises used: Equiv.symm_apply_apply, Option.some, Subtype.val
-- 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 }
a : α
⊢ ((↑e : Option α ≃ β).symm : (a : β) → Option α)
      (↑((fun (a : α) ↦
              (Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯ :
                { y : β // y ≠ x }))
            a) :
        β) =
    some a

Tactic:
exact symm_apply_apply (e : Option α ≃ β) a

Premises used: Equiv.symm_apply_apply, Option.some, Subtype.val