awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a₁
h₂ : Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a₂
h : Eq.{u + 1} (α := Option α) ((f.symm : (a : β) → Option α) b : Option α) (none : Option α)
⊢ a₁ = a₂

Tactic:
simp_all
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a₁
h₂ : Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a₂
val : α
h : (f.symm : (a : β) → Option α) b = some val
⊢ a₁ = a₂

Tactic:
simp_all
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome.{v} (α := β) ((f : (a : α) → Option β) a₁) = true
x : α
none :
  ∀ (hfx : Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) x : Option β) (Option.none : Option β)),
    (fun (b : Option β) ↦
          (Option.recOn (motive := fun (x : Option β) ↦ α) b a₂ fun (b' : β) ↦
              Option.recOn (motive := fun (x : Option α) ↦ α) ((f.symm : (a : β) → Option α) b') a₂ id :
            α))
        Option.none =
      x
some :
  ∀ (val : β) (hfx : (f : (a : α) → Option β) x = Option.some val),
    (fun (b : Option β) ↦
          (Option.recOn (motive := fun (x : Option β) ↦ α) b a₂ fun (b' : β) ↦
              Option.recOn (motive := fun (x : Option α) ↦ α) ((f.symm : (a : β) → Option α) b') a₂ id :
            α))
        (Option.some val) =
      x
⊢ (fun (b : Option β) ↦
        (Option.recOn (motive := fun (x : Option β) ↦ α) b a₂ fun (b' : β) ↦
            Option.recOn (motive := fun (x : Option α) ↦ α) ((f.symm : (a : β) → Option α) b') a₂ id :
          α))
      ((f : (a : α) → Option β) x) =
    x

Tactic:
cases hfx : f x

Premises used: DFunLike.coe
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome.{v} (α := β) ((f : (a : α) → Option β) a₁) = true
x : α
hfx : Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) x : Option β) (none : Option β)
⊢ ¬isSome.{v} (α := β) none = true

Tactic:
simp
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome.{v} (α := β) ((f : (a : α) → Option β) a₁) = true
x : α
hfx : Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) x : Option β) (none : Option β)
⊢ x = a₂

Tactic:
have : x = a₂ := not_imp_comm.1 (h x) (hfx.symm ▸ by simp)
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome.{v} (α := β) ((f : (a : α) → Option β) a₁) = true
x : α
hfx : Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) x : Option β) (none : Option β)
this : x = a₂
⊢ (fun (b : Option β) ↦
        (Option.recOn (motive := fun (x : Option β) ↦ α) b a₂ fun (b' : β) ↦
            Option.recOn (motive := fun (x : Option α) ↦ α) ((f.symm : (a : β) → Option α) b') a₂ id :
          α))
      none =
    x

Tactic:
simp [this]
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome.{v} (α := β) ((f : (a : α) → Option β) a₁) = true
x : α
val : β
hfx : (f : (a : α) → Option β) x = Option.some val
some : Option.rec (motive := fun (x : Option α) ↦ α) a₂ id ((f.symm : (a : β) → Option α) val) = x
⊢ (fun (b : Option β) ↦
        (Option.recOn (motive := fun (x : Option β) ↦ α) b a₂ fun (b' : β) ↦
            Option.recOn (motive := fun (x : Option α) ↦ α) ((f.symm : (a : β) → Option α) b') a₂ id :
          α))
      (Option.some val) =
    x

Tactic:
dsimp only
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome.{v} (α := β) ((f : (a : α) → Option β) a₁) = true
x : α
val : β
hfx : (f : (a : α) → Option β) x = Option.some val
some : Option.rec (motive := fun (x : Option α) ↦ α) a₂ id (Option.some x) = x
⊢ Option.rec (motive := fun (x : Option α) ↦ α) a₂ id ((f.symm : (a : β) → Option α) val) = x

Tactic:
rw [(eq_some_iff f).2 hfx]

Premises used: Iff.mpr, PEquiv.eq_some_iff
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome.{v} (α := β) ((f : (a : α) → Option β) a₁) = true
x : α
val : β
hfx : (f : (a : α) → Option β) x = some val
⊢ Option.rec (motive := fun (x : Option α) ↦ α) a₂ id (some x) = x

Tactic:
rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome.{v} (α := β) ((f : (a : α) → Option β) a₁) = true
x : α
none :
  ∀ (hfx : Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) x : Option β) (Option.none : Option β)),
    (fun (b : Option β) ↦
          (Option.recOn (motive := fun (x : Option β) ↦ α) b a₂ fun (b' : β) ↦
              Option.recOn (motive := fun (x : Option α) ↦ α) ((f.symm : (a : β) → Option α) b') a₂ id :
            α))
        Option.none =
      x
some some₁ :
  ∀ (val : β) (hfx : (f : (a : α) → Option β) x = Option.some val),
    (fun (b : Option β) ↦
          (Option.recOn (motive := fun (x : Option β) ↦ α) b a₂ fun (b' : β) ↦
              Option.recOn (motive := fun (x : Option α) ↦ α) ((f.symm : (a : β) → Option α) b') a₂ id :
            α))
        (Option.some val) =
      x
⊢ (fun (b : Option β) ↦
        (Option.recOn (motive := fun (x : Option β) ↦ α) b a₂ fun (b' : β) ↦
            Option.recOn (motive := fun (x : Option α) ↦ α) ((f.symm : (a : β) → Option α) b') a₂ id :
          α))
      ((f : (a : α) → Option β) x) =
    x

Tactic:
classical
        cases hfx : f x
        · have : x = a₂ := not_imp_comm.1 (h x) (hfx.symm ▸ by simp)
          simp [this]
        · dsimp only
          rw [(eq_some_iff f).2 hfx]
          rfl

Premises used: DFunLike.coe
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
h : ∀ (a : α), isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true
⊢ Injective.{u + 1, v + 1} (α := α) (β := Option β) (⇑f : (a : α) → Option β)

Tactic:
(Classical.em (Nonempty α)).elim
    (fun hn => injective_of_forall_ne_isSome f (Classical.choice hn) fun a _ => h a) fun hn x =>
    (hn ⟨x⟩).elim

Premises used: False.elim, PEquiv.injective_of_forall_ne_isSome, Classical.choice, Nonempty.intro, Classical.em, Nonempty, Or.elim
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
s_1 : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s_1
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
a b : α
pos : ∀ (hb : b ∈ s) (ha : a ∈ s), some b = some a ↔ some a = some b
neg : ∀ (hb : b ∈ s) (ha : ¬a ∈ s), some b = some a ↔ False
pos₁ : ∀ (hb : ¬b ∈ s) (ha : a ∈ s), False ↔ some a = some b
neg₁ : ∀ (hb : ¬b ∈ s) (ha : ¬a ∈ s), False ↔ False
⊢ (if b ∈ s then some b else none) = some a ↔ (if a ∈ s then some a else none) = some b

Tactic:
split_ifs with hb ha ha
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
s_1 : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s_1
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
a b : α
hb : b ∈ s
ha : a ∈ s
⊢ some b = some a ↔ some a = some b

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
s_1 : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s_1
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
a b : α
hb : b ∈ s
ha : ¬a ∈ s
⊢ some b = some a ↔ False

Tactic:
simp [ne_of_mem_of_not_mem hb ha]

Premises used: ne_of_mem_of_not_mem
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
s_1 : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s_1
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
a b : α
hb : ¬b ∈ s
ha : a ∈ s
⊢ False ↔ some a = some b

Tactic:
simp [ne_of_mem_of_not_mem ha hb]

Premises used: ne_of_mem_of_not_mem
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
s_1 : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s_1
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
a b : α
hb : ¬b ∈ s
ha : ¬a ∈ s
⊢ False ↔ False

Tactic:
simp
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
dsimp : (a ∈ if a ∈ s then some a else none) ↔ a ∈ s
⊢ Membership.mem (γ := Option α) ((ofSet s : (a : α) → Option α) a : Option α) a ↔ a ∈ s

Tactic:
dsimp [ofSet]

Premises used: PEquiv.ofSet
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
pos : a ∈ s → (a ∈ some a ↔ a ∈ s)
neg : ¬a ∈ s → (Membership.mem (γ := Option α) none a ↔ a ∈ s)
⊢ (a ∈ if a ∈ s then some a else none) ↔ a ∈ s

Tactic:
split_ifs
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
h : a ∈ s
⊢ a ∈ some a ↔ a ∈ s

Tactic:
simp [*]
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
h : ¬a ∈ s
⊢ Membership.mem (γ := Option α) none a ↔ a ∈ s

Tactic:
simp [*]
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a b : α
dsimp : (a ∈ if b ∈ s then some b else none) ↔ a = b ∧ a ∈ s
⊢ Membership.mem (γ := Option α) ((ofSet s : (a : α) → Option α) b : Option α) a ↔ a = b ∧ a ∈ s

Tactic:
dsimp [ofSet]

Premises used: PEquiv.ofSet
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a b : α
⊢ (a ∈ if b ∈ s then some b else none) ↔ a = b ∧ a ∈ s

Tactic:
grind
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
x : DecidablePred fun (x : α) ↦ x ∈ s
a b : α
⊢ (ofSet s : (a : α) → Option α) b = some a ↔ a = b ∧ a ∈ s

Tactic:
mem_ofSet_iff

Premises used: PEquiv.mem_ofSet_iff
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
x : DecidablePred fun (x : α) ↦ x ∈ s
a : α
⊢ (ofSet s : (a : α) → Option α) a = some a ↔ a ∈ s

Tactic:
mem_ofSet_self_iff

Premises used: PEquiv.mem_ofSet_self_iff
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
⊢ (ofSet s).symm = ofSet s

Tactic:
rfl

Premises used: PEquiv.ofSet, PEquiv.symm, rfl, ite
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
⊢ ofSet Set.univ = PEquiv.refl α

Tactic:
rfl

Premises used: PEquiv.ofSet, PEquiv.refl, rfl, ite
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
h : ofSet s = PEquiv.refl α
rw : ∀ (x : α), x ∈ s
⊢ s = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
h : ofSet s = PEquiv.refl α
x : α
rw : Membership.mem (γ := Option α) ((PEquiv.refl α : (a : α) → Option α) x : Option α) x
⊢ x ∈ s

Tactic:
rw [← mem_ofSet_self_iff, h]

Premises used: PEquiv.mem_ofSet_self_iff
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
h : ofSet s = PEquiv.refl α
x : α
⊢ Membership.mem (γ := Option α) ((PEquiv.refl α : (a : α) → Option α) x : Option α) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
h : ofSet s = PEquiv.refl α
x : α
⊢ Membership.mem (γ := Option α) ((PEquiv.refl α : (a : α) → Option α) x : Option α) x

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
h : s = Set.univ
⊢ ofSet s = PEquiv.refl α

Tactic:
simp only [← ofSet_univ, h]

Premises used: PEquiv.ofSet_univ
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
⊢ (f.trans g).symm = g.symm.trans f.symm

Tactic:
rfl

Premises used: PEquiv.symm, rfl, PEquiv.trans
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
h :
  ∀ (x a : α),
    (f.trans f.symm : (a : α) → Option α) x = some a ↔
      (ofSet {a : α | isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true} : (a : α) → Option α) x = some a
⊢ f.trans f.symm = ofSet {a : α | isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true}

Tactic:
ext
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
x a : α
h :
  Option.bind.{v, u} (α := β) ((f : (a : α) → Option β) x) (⇑f.symm : (a : β) → Option α) = some a ↔
    (ofSet {a : α | isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true} : (a : α) → Option α) x = some a
⊢ (f.trans f.symm : (a : α) → Option α) x = some a ↔
    (ofSet {a : α | isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true} : (a : α) → Option α) x = some a

Tactic:
dsimp [PEquiv.trans]

Premises used: PEquiv.trans
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
x a : α
h :
  (∃ (a_1 : β), (f : (a : α) → Option β) x = some a_1 ∧ (f : (a : α) → Option β) a = some a_1) ↔
    a = x ∧ Membership.mem (γ := Set α) {a : α | ∃ (a_1 : β), (f : (a : α) → Option β) a = some a_1} a
⊢ Option.bind.{v, u} (α := β) ((f : (a : α) → Option β) x) (⇑f.symm : (a : β) → Option α) = some a ↔
    (ofSet {a : α | isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true} : (a : α) → Option α) x = some a

Tactic:
simp only [eq_some_iff f, Option.isSome_iff_exists, bind_eq_some_iff,
    ofSet_eq_some_iff]

Premises used: PEquiv.ofSet_eq_some_iff, Option.isSome_iff_exists, PEquiv.eq_some_iff, Option.bind_eq_some_iff
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
x a : α
h :
  (∃ (a_1 : β), (f : (a : α) → Option β) x = some a_1 ∧ (f : (a : α) → Option β) a = some a_1) →
    a = x ∧ Membership.mem (γ := Set α) {a : α | ∃ (a_2 : β), (f : (a : α) → Option β) a = some a_2} a
h₁ :
  a = x ∧ Membership.mem (γ := Set α) {a : α | ∃ (a_1 : β), (f : (a : α) → Option β) a = some a_1} a →
    ∃ (a_2 : β), (f : (a : α) → Option β) x = some a_2 ∧ (f : (a : α) → Option β) a = some a_2
⊢ (∃ (a_1 : β), (f : (a : α) → Option β) x = some a_1 ∧ (f : (a : α) → Option β) a = some a_1) ↔
    a = x ∧ Membership.mem (γ := Set α) {a : α | ∃ (a_1 : β), (f : (a : α) → Option β) a = some a_1} a

Tactic:
constructor
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
x a : α
b : β
hb₁ : (f : (a : α) → Option β) x = some b
hb₂ : (f : (a : α) → Option β) a = some b
⊢ a = x ∧ Membership.mem (γ := Set α) {a : α | ∃ (a_1 : β), (f : (a : α) → Option β) a = some a_1} a

Tactic:
⟨PEquiv.inj _ hb₂ hb₁, b, hb₂⟩

Premises used: PEquiv.inj, And.intro, Exists.intro
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
x a : α
b : β
hb₁ : (f : (a : α) → Option β) x = some b
hb₂ : (f : (a : α) → Option β) a = some b
⊢ a = x ∧ Membership.mem (γ := Set α) {a : α | ∃ (a_1 : β), (f : (a : α) → Option β) a = some a_1} a

Tactic:
exact ⟨PEquiv.inj _ hb₂ hb₁, b, hb₂⟩
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
x a : α
⊢ a = x ∧ Membership.mem (γ := Set α) {a : α | ∃ (a_1 : β), (f : (a : α) → Option β) a = some a_1} a →
    ∃ (a_2 : β), (f : (a : α) → Option β) x = some a_2 ∧ (f : (a : α) → Option β) a = some a_2

Tactic:
simp +contextual
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
⊢ (f.symm.trans f).symm = PEquiv.symm (ofSet {b : β | isSome.{u} (α := α) ((f.symm : (a : β) → Option α) b) = true})

Tactic:
simp [symm_trans_rev, self_trans_symm, -symm_symm]

Premises used: PEquiv.symm_symm, PEquiv.symm_trans_rev, PEquiv.self_trans_symm
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
rw :
  (∀ (x : α), Membership.mem (γ := Set α) {a : α | isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true} x) ↔
    ∀ (a : α), isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true
⊢ f.trans f.symm = PEquiv.refl α ↔ ∀ (a : α), isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true

Tactic:
rw [self_trans_symm, ofSet_eq_refl, Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall, PEquiv.self_trans_symm, PEquiv.ofSet_eq_refl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
⊢ (∀ (x : α), Membership.mem (γ := Set α) {a : α | isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true} x) ↔
    ∀ (a : α), isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true

Tactic:
rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
⊢ ∀ (a : α) (b : β), none = some a ↔ none = some b

Tactic:
simp
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
a : α
⊢ Eq.{v + 1} (α := Option β) (((⊥ : α ≃. β) : (a : α) → Option β) a : Option β) (none : Option β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
⊢ Eq (α := β ≃. α) (PEquiv.symm ⊥) ⊥

Tactic:
rfl

Premises used: PEquiv.symm, rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
h : ∀ (x : α) (a : γ), (f.trans ⊥ : (a : α) → Option γ) x = some a ↔ ((⊥ : α ≃. γ) : (a : α) → Option γ) x = some a
⊢ Eq (α := α ≃. γ) (f.trans ⊥) ⊥

Tactic:
ext
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
x : α
a : γ
h : Option.bind.{v, w} (α := β) ((f : (a : α) → Option β) x) (⇑⊥ : (a : β) → Option γ) = some a ↔ none = some a
⊢ (f.trans ⊥ : (a : α) → Option γ) x = some a ↔ ((⊥ : α ≃. γ) : (a : α) → Option γ) x = some a

Tactic:
dsimp [PEquiv.trans]

Premises used: PEquiv.trans
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
x : α
a : γ
⊢ Option.bind.{v, w} (α := β) ((f : (a : α) → Option β) x) (⇑⊥ : (a : β) → Option γ) = some a ↔ none = some a

Tactic:
simp
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
f : β ≃. γ
h :
  ∀ (x : α) (a : γ), (PEquiv.trans ⊥ f : (a : α) → Option γ) x = some a ↔ ((⊥ : α ≃. γ) : (a : α) → Option γ) x = some a
⊢ Eq (α := α ≃. γ) (PEquiv.trans ⊥ f) ⊥

Tactic:
ext
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
f : β ≃. γ
x : α
a : γ
⊢ none = some a ↔ none = some a

Tactic:
simp
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a : α
h : isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true
rw : (f : (a : α) → Option β) a = some (Option.get ((f : (a : α) → Option β) a) h)
rw₁ rw₂ : Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) ((f : (a : α) → Option β) a : Option β)
⊢ (f.symm : (a : β) → Option α) (Option.get ((f : (a : α) → Option β) a) h) = some a

Tactic:
rw [f.eq_some_iff, some_get]

Premises used: Option.some_get, PEquiv.eq_some_iff
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
pos : ∀ (h1 : y = b) (h2 : x = a), some a = some x ↔ some b = some y
neg : ∀ (h1 : y = b) (h2 : ¬x = a), some a = some x ↔ False
pos₁ : ∀ (h1 : ¬y = b), x = a → (False ↔ some b = some y)
neg₁ : ∀ (h1 : ¬y = b), ¬x = a → (False ↔ False)
⊢ (if y = b then some a else none) = some x ↔ (if x = a then some b else none) = some y

Tactic:
split_ifs with h1 h2
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : y = b
h2 : x = a
⊢ some a = some x ↔ some b = some y

Tactic:
simp [*]
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : y = b
h2 : ¬x = a
neg : ¬a = x
⊢ some a = some x ↔ False

Tactic:
simp only [some.injEq, iff_false] at *

Premises used: iff_false, Option.some.injEq
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : y = b
h2 : ¬x = a
⊢ ¬a = x

Tactic:
Ne.symm h2

Premises used: Ne.symm
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : y = b
h2 : ¬x = a
⊢ ¬a = x

Tactic:
exact Ne.symm h2

Premises used: Ne.symm
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : ¬y = b
h : x = a
pos : ¬b = y
⊢ False ↔ some b = some y

Tactic:
simp only [some.injEq, false_iff] at *

Premises used: Option.some.injEq, false_iff
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : ¬y = b
h : x = a
⊢ ¬b = y

Tactic:
Ne.symm h1

Premises used: Ne.symm
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : ¬y = b
h : x = a
⊢ ¬b = y

Tactic:
exact Ne.symm h1

Premises used: Ne.symm
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : ¬y = b
h : ¬x = a
⊢ False ↔ False

Tactic:
simp
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
a : α
b : β
⊢ Membership.mem (γ := Option β) ((single a b : (a : α) → Option β) a : Option β) b

Tactic:
if_pos rfl

Premises used: if_pos, rfl, ite
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
dsimp : (b₁ ∈ if a₁ = a₂ then some b₂ else none) ↔ a₁ = a₂ ∧ b₁ = b₂
⊢ Membership.mem (γ := Option β) ((single a₂ b₂ : (a : α) → Option β) a₁ : Option β) b₁ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
dsimp [single]

Premises used: PEquiv.single
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
pos : a₁ = a₂ → (b₁ ∈ some b₂ ↔ a₁ = a₂ ∧ b₁ = b₂)
neg : ¬a₁ = a₂ → (Membership.mem (γ := Option β) none b₁ ↔ a₁ = a₂ ∧ b₁ = b₂)
⊢ (b₁ ∈ if a₁ = a₂ then some b₂ else none) ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
split_ifs
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
h : a₁ = a₂
⊢ b₁ ∈ some b₂ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
simp [*, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
h : ¬a₁ = a₂
⊢ Membership.mem (γ := Option β) none b₁ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
simp [*, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
a : α
b : β
⊢ (single a b).symm = single b a

Tactic:
rfl

Premises used: PEquiv.single, PEquiv.symm, rfl, ite
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
a : α
b : β
⊢ (single a b : (a : α) → Option β) a = some b

Tactic:
if_pos rfl

Premises used: if_pos, rfl, ite
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : DecidableEq β
a₁ a₂ : α
h : a₁ ≠ a₂
b : β
⊢ Eq.{v + 1} (α := Option β) ((single a₁ b : (a : α) → Option β) a₂ : Option β) (none : Option β)

Tactic:
if_neg h.symm

Premises used: Ne.symm, if_neg, ite
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : Membership.mem (γ := Option γ) ((f : (a : β) → Option γ) b : Option γ) c
h₁ :
  ∀ (x : α) (a_1 : γ),
    ((single a b).trans f : (a : α) → Option γ) x = some a_1 ↔ (single a c : (a : α) → Option γ) x = some a_1
⊢ (single a b).trans f = single a c

Tactic:
ext
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : Membership.mem (γ := Option γ) ((f : (a : β) → Option γ) b : Option γ) c
x : α
a_1 : γ
h₁ :
  (if x = a then some b else none).bind (⇑f : (a : β) → Option γ) = some a_1 ↔
    (if x = a then some c else none) = some a_1
⊢ ((single a b).trans f : (a : α) → Option γ) x = some a_1 ↔ (single a c : (a : α) → Option γ) x = some a_1

Tactic:
dsimp [single, PEquiv.trans]

Premises used: PEquiv.single, PEquiv.trans