awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : γ
pos : x = a → (((some b).bind fun (a : β) ↦ (f : (a : β) → Option γ) a) = some a_1 ↔ some c = some a_1)
neg : ¬x = a → ((Option.bind none fun (a : β) ↦ (f : (a : β) → Option γ) a) = some a_1 ↔ False)
⊢ (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

Tactic:
split_ifs
-- 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_1 : x = a
⊢ ((some b).bind fun (a : β) ↦ (f : (a : β) → Option γ) a) = some a_1 ↔ some c = some a_1

Tactic:
simp_all
-- 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_1 : ¬x = a
⊢ (Option.bind none fun (a : β) ↦ (f : (a : β) → Option γ) a) = some a_1 ↔ False

Tactic:
simp_all
-- 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 β) a : Option β) b
⊢ f.trans (single b c) = single a c

Tactic:
symm_injective <| single_trans_of_mem _ ((mem_iff_mem f).2 h)

Premises used: Iff.mpr, PEquiv.mem_iff_mem, PEquiv.symm_injective, PEquiv.single_trans_of_mem
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
⊢ (single a b).trans (single b c) = single a c

Tactic:
single_trans_of_mem _ (mem_single _ _)

Premises used: PEquiv.mem_single, PEquiv.single_trans_of_mem
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Subsingleton α
a b : α
h : ∀ (i j : α), (single a b : (a : α) → Option α) i = some j ↔ (PEquiv.refl α : (a : α) → Option α) i = some j
⊢ single a b = PEquiv.refl α

Tactic:
ext i j
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Subsingleton α
a b i j : α
h : (if i = a then some b else none) = some j ↔ some i = some j
⊢ (single a b : (a : α) → Option α) i = some j ↔ (PEquiv.refl α : (a : α) → Option α) i = some j

Tactic:
dsimp [single]

Premises used: PEquiv.single
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Subsingleton α
a b i j : α
h : some b = some j ↔ some i = some j
h₁ : some b = some j ↔ some j = some j
h₂ h₃ : some j = some j ↔ some j = some j
⊢ (if i = a then some b else none) = some j ↔ some i = some j

Tactic:
rw [if_pos (Subsingleton.elim i a), Subsingleton.elim i j, Subsingleton.elim b j]

Premises used: if_pos, Subsingleton.elim
-- Module: Mathlib.Data.PEquiv
Goal:
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq β
inst_1 : DecidableEq γ
b : β
c : γ
f : δ ≃. β
h : Eq.{x + 1} (α := Option δ) ((f.symm : (a : β) → Option δ) b : Option δ) (none : Option δ)
h₁ :
  ∀ (x : δ) (a : γ),
    (f.trans (single b c) : (a : δ) → Option γ) x = some a ↔ ((⊥ : δ ≃. γ) : (a : δ) → Option γ) x = some a
⊢ f.trans (single b c) = ⊥

Tactic:
ext
-- Module: Mathlib.Data.PEquiv
Goal:
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq β
inst_1 : DecidableEq γ
b : β
c : γ
f : δ ≃. β
h : Eq.{x + 1} (α := Option δ) ((f.symm : (a : β) → Option δ) b : Option δ) (none : Option δ)
x : δ
a : γ
⊢ ∀ (a : δ), ¬(f : (a : δ) → Option β) a = some b

Tactic:
simp only [eq_none_iff_forall_not_mem, Option.mem_def, f.eq_some_iff] at h

Premises used: PEquiv.eq_some_iff, Option.eq_none_iff_forall_not_mem, Option.mem_def
-- Module: Mathlib.Data.PEquiv
Goal:
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq β
inst_1 : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x : δ
a : γ
h : ∀ (a : δ), ¬(f : (a : δ) → Option β) a = some b
h₁ : (Option.bind ((f : (a : δ) → Option β) x) fun (x : β) ↦ if x = b then some c else none) = some a ↔ none = some a
⊢ (f.trans (single b c) : (a : δ) → Option γ) x = some a ↔ ((⊥ : δ ≃. γ) : (a : δ) → Option γ) x = some a

Tactic:
dsimp [PEquiv.trans, single]

Premises used: PEquiv.single, PEquiv.trans
-- Module: Mathlib.Data.PEquiv
Goal:
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq β
inst_1 : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x : δ
a : γ
h : ∀ (a : δ), ¬(f : (a : δ) → Option β) a = some b
h₁ : ∀ (x_1 : β), (f : (a : δ) → Option β) x = some x_1 → ¬(if x_1 = b then some c else none) = some a
⊢ (Option.bind ((f : (a : δ) → Option β) x) fun (x : β) ↦ if x = b then some c else none) = some a ↔ none = some a

Tactic:
simp only [bind_eq_some_iff, iff_false, not_exists, not_and, reduceCtorEq]

Premises used: reduceCtorEq, iff_false, not_exists, Option.bind_eq_some_iff, not_and
-- Module: Mathlib.Data.PEquiv
Goal:
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq β
inst_1 : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x : δ
a : γ
h : ∀ (a : δ), ¬(f : (a : δ) → Option β) a = some b
x_1 : β
h_1 : (f : (a : δ) → Option β) x = some x_1
pos : x_1 = b → ¬some c = some a
neg : ¬x_1 = b → ¬False
⊢ ¬(if x_1 = b then some c else none) = some a

Tactic:
split_ifs
-- Module: Mathlib.Data.PEquiv
Goal:
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq β
inst_1 : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x : δ
a : γ
h : ∀ (a : δ), ¬(f : (a : δ) → Option β) a = some b
x_1 : β
h_1 : (f : (a : δ) → Option β) x = some x_1
h_2 : x_1 = b
⊢ ¬some c = some a

Tactic:
simp_all
-- Module: Mathlib.Data.PEquiv
Goal:
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq β
inst_1 : DecidableEq γ
b : β
c : γ
f : δ ≃. β
x : δ
a : γ
h : ∀ (a : δ), ¬(f : (a : δ) → Option β) a = some b
x_1 : β
h_1 : (f : (a : δ) → Option β) x = some x_1
h_2 : ¬x_1 = b
⊢ ¬False

Tactic:
simp_all
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
a : α
b : β
f : β ≃. δ
h : Eq.{x + 1} (α := Option δ) ((f : (a : β) → Option δ) b : Option δ) (none : Option δ)
⊢ (single a b).trans f = ⊥

Tactic:
symm_injective <| trans_single_of_eq_none _ h

Premises used: PEquiv.trans_single_of_eq_none, PEquiv.symm_injective
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
b₁ b₂ : β
h : b₁ ≠ b₂
a : α
c : γ
⊢ (single a b₁).trans (single b₂ c) = ⊥

Tactic:
single_trans_of_eq_none _ (single_apply_of_ne h.symm _)

Premises used: PEquiv.single_trans_of_eq_none, PEquiv.single_apply_of_ne, Ne.symm
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
gf :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
a : α
none :
  ∀ (h : Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β) (Option.none : Option β)),
    Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) (Option.none : Option β)
some : ∀ (b : β) (h : (g : (a : α) → Option β) a = Option.some b), (f : (a : α) → Option β) a = Option.some b
⊢ Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) ((g : (a : α) → Option β) a : Option β)

Tactic:
rcases h : g a with _ | b

Premises used: DFunLike.coe
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
gf :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
a : α
h : Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β) (none : Option β)
⊢ Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) (none : Option β)

Tactic:
eq_none_iff_forall_not_mem.2 fun b hb => Option.not_mem_none b <| h ▸ fg a b hb

Premises used: Iff.mpr, Eq.rec, Option.eq_none_iff_forall_not_mem, Option.not_mem_none
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
gf :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
a : α
h : Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β) (none : Option β)
⊢ Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) (none : Option β)

Tactic:
exact eq_none_iff_forall_not_mem.2 fun b hb => Option.not_mem_none b <| h ▸ fg a b hb

Premises used: Iff.mpr, Option.eq_none_iff_forall_not_mem, Option.not_mem_none
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
gf :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
a : α
b : β
h : (g : (a : α) → Option β) a = some b
⊢ (f : (a : α) → Option β) a = some b

Tactic:
gf _ _ h
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
gf :
  ∀ (a : α) (b : β),
    Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b →
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
a : α
b : β
h : (g : (a : α) → Option β) a = some b
⊢ (f : (a : α) → Option β) a = some b

Tactic:
exact gf _ _ h
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f g : α ≃. β
⊢ f ≤ g ↔
    ∀ (a : α) (b : β),
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b →
        Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g : α ≃. β
a : α
b : β
⊢ Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a ↔
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b

Tactic:
have hf := @mem_iff_mem _ _ f a b
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g : α ≃. β
a : α
b : β
hf :
  Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a ↔
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
⊢ Membership.mem (γ := Option α) ((g.symm : (a : β) → Option α) b : Option α) a ↔
    Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b

Tactic:
have hg := @mem_iff_mem _ _ g a b
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g : α ≃. β
a : α
b : β
hf :
  Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a ↔
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
hg :
  Membership.mem (γ := Option α) ((g.symm : (a : β) → Option α) b : Option α) a ↔
    Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
⊢ (f.symm : (a : β) → Option α) b = some a ↔ (f : (a : α) → Option β) a = some b

Tactic:
simp only [Option.mem_def] at *

Premises used: Option.mem_def
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g : α ≃. β
a : α
b : β
hf :
  Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a ↔
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
hg :
  Membership.mem (γ := Option α) ((g.symm : (a : β) → Option α) b : Option α) a ↔
    Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
hf₁ : (f.symm : (a : β) → Option α) b = some a ↔ (f : (a : α) → Option β) a = some b
⊢ (g.symm : (a : β) → Option α) b = some a ↔ (g : (a : α) → Option β) a = some b

Tactic:
simp only [Option.mem_def] at *

Premises used: Option.mem_def
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g : α ≃. β
a : α
b : β
hf : (f.symm : (a : β) → Option α) b = some a ↔ (f : (a : α) → Option β) a = some b
hg : (g.symm : (a : β) → Option α) b = some a ↔ (g : (a : α) → Option β) a = some b
⊢ (if
          Eq.{u + 1} (α := Option α) ((f.symm : (a : β) → Option α) b : Option α)
            ((g.symm : (a : β) → Option α) b : Option α) then
        (f.symm : (a : β) → Option α) b
      else none) =
      some a ↔
    (if Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) a : Option β) ((g : (a : α) → Option β) a : Option β) then
        (f : (a : α) → Option β) a
      else none) =
      some b

Tactic:
grind
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
simp :
  (if
          Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β)
            ((x_1 : (a : α) → Option β) x_2 : Option β) then
        (x : (a : α) → Option β) x_2
      else none) =
      some x_3 →
    (x : (a : α) → Option β) x_2 = some x_3
⊢ Membership.mem (γ := Option β)
      (({
              toFun := fun (a : α) ↦
                if
                    Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) a : Option β)
                      ((x_1 : (a : α) → Option β) a : Option β) then
                  (x : (a : α) → Option β) a
                else none,
              invFun := fun (b : β) ↦
                if
                    Eq.{u + 1} (α := Option α) ((x.symm : (a : β) → Option α) b : Option α)
                      ((x_1.symm : (a : β) → Option α) b : Option α) then
                  (x.symm : (a : β) → Option α) b
                else none,
              inv := ⋯ } :
            (a : α) → Option β)
          x_2 :
        Option β)
      x_3 →
    Membership.mem (γ := Option β) ((x : (a : α) → Option β) x_2 : Option β) x_3

Tactic:
simp only [coe_mk, mem_def]

Premises used: PEquiv.coe_mk, Option.mem_def
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
pos :
  Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β) →
    (x : (a : α) → Option β) x_2 = some x_3 → (x : (a : α) → Option β) x_2 = some x_3
neg :
  ¬Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β) →
    False → (x : (a : α) → Option β) x_2 = some x_3
⊢ (if
          Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β)
            ((x_1 : (a : α) → Option β) x_2 : Option β) then
        (x : (a : α) → Option β) x_2
      else none) =
      some x_3 →
    (x : (a : α) → Option β) x_2 = some x_3

Tactic:
split_ifs
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
h : Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β)
⊢ (x : (a : α) → Option β) x_2 = some x_3 → (x : (a : α) → Option β) x_2 = some x_3

Tactic:
simp [*]
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
h : ¬Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β)
⊢ False → (x : (a : α) → Option β) x_2 = some x_3

Tactic:
simp [*]
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
simp :
  (if
          Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β)
            ((x_1 : (a : α) → Option β) x_2 : Option β) then
        (x : (a : α) → Option β) x_2
      else none) =
      some x_3 →
    (x_1 : (a : α) → Option β) x_2 = some x_3
⊢ Membership.mem (γ := Option β)
      (({
              toFun := fun (a : α) ↦
                if
                    Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) a : Option β)
                      ((x_1 : (a : α) → Option β) a : Option β) then
                  (x : (a : α) → Option β) a
                else none,
              invFun := fun (b : β) ↦
                if
                    Eq.{u + 1} (α := Option α) ((x.symm : (a : β) → Option α) b : Option α)
                      ((x_1.symm : (a : β) → Option α) b : Option α) then
                  (x.symm : (a : β) → Option α) b
                else none,
              inv := ⋯ } :
            (a : α) → Option β)
          x_2 :
        Option β)
      x_3 →
    Membership.mem (γ := Option β) ((x_1 : (a : α) → Option β) x_2 : Option β) x_3

Tactic:
simp only [coe_mk, mem_def]

Premises used: PEquiv.coe_mk, Option.mem_def
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
pos :
  Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β) →
    (x : (a : α) → Option β) x_2 = some x_3 → (x_1 : (a : α) → Option β) x_2 = some x_3
neg :
  ¬Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β) →
    False → (x_1 : (a : α) → Option β) x_2 = some x_3
⊢ (if
          Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β)
            ((x_1 : (a : α) → Option β) x_2 : Option β) then
        (x : (a : α) → Option β) x_2
      else none) =
      some x_3 →
    (x_1 : (a : α) → Option β) x_2 = some x_3

Tactic:
split_ifs
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
h : Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β)
⊢ (x : (a : α) → Option β) x_2 = some x_3 → (x_1 : (a : α) → Option β) x_2 = some x_3

Tactic:
simp [*]
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
h : ¬Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β)
⊢ False → (x_1 : (a : α) → Option β) x_2 = some x_3

Tactic:
simp [*]
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
⊢ Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b

Tactic:
have hf := fg a b H
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
hf : Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
⊢ Membership.mem (γ := Option β) ((h : (a : α) → Option β) a : Option β) b

Tactic:
have hg := gh a b H
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
hf : Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
hg : Membership.mem (γ := Option β) ((h : (a : α) → Option β) a : Option β) b
simp :
  ∀ (H : (f : (a : α) → Option β) a = some b) (hf : (g : (a : α) → Option β) a = some b)
    (hg : (h : (a : α) → Option β) a = some b),
    (if Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β) ((h : (a : α) → Option β) a : Option β) then
        (g : (a : α) → Option β) a
      else none) =
      some b
⊢ Membership.mem (γ := Option β)
    (({
            toFun := fun (a : α) ↦
              if
                  Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β)
                    ((h : (a : α) → Option β) a : Option β) then
                (g : (a : α) → Option β) a
              else none,
            invFun := fun (b : β) ↦
              if
                  Eq.{u + 1} (α := Option α) ((g.symm : (a : β) → Option α) b : Option α)
                    ((h.symm : (a : β) → Option α) b : Option α) then
                (g.symm : (a : β) → Option α) b
              else none,
            inv := ⋯ } :
          (a : α) → Option β)
        a :
      Option β)
    b

Tactic:
simp only [Option.mem_def, PEquiv.coe_mk_apply] at *

Premises used: PEquiv.coe_mk_apply, Option.mem_def
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : (f : (a : α) → Option β) a = some b
hf : (g : (a : α) → Option β) a = some b
hg : (h : (a : α) → Option β) a = some b
rw : (if some b = (h : (a : α) → Option β) a then some b else none) = some b
rw₁ : (if some b = some b then some b else none) = some b
rw₂ rw₃ : some b = some b
⊢ (if Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β) ((h : (a : α) → Option β) a : Option β) then
      (g : (a : α) → Option β) a
    else none) =
    some b

Tactic:
rw [hf, hg, if_pos rfl]

Premises used: if_pos, rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ≃ β
⊢ ∀ (a : α) (b : β), (some ∘ (⇑f.symm : (a : β) → α)) b = some a ↔ (some ∘ (⇑f : (a : α) → β)) a = some b

Tactic:
simp [Equiv.eq_symm_apply, eq_comm]

Premises used: eq_comm, Equiv.eq_symm_apply
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u_1
⊢ (Equiv.refl α).toPEquiv = PEquiv.refl α

Tactic:
rfl

Premises used: Equiv.toPEquiv, PEquiv.refl, rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ≃ β
g : β ≃ γ
⊢ (f.trans g).toPEquiv = f.toPEquiv.trans g.toPEquiv

Tactic:
rfl

Premises used: rfl, PEquiv.trans
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u_1
β : Type u_2
f : α ≃ β
⊢ f.symm.toPEquiv = f.toPEquiv.symm

Tactic:
rfl

Premises used: Equiv.toPEquiv, PEquiv.symm, rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u_1
β : Type u_2
f : α ≃ β
x : α
⊢ Eq.{u_2 + 1} (α := Option β) ((f.toPEquiv : (a : α) → Option β) x : Option β) (some ((f : (a : α) → β) x) : Option β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
x : α
⊢ x ∈ f.Dom ↔ ∃ (y : β), y ∈ f x

Tactic:
simp [Dom, Part.dom_iff_mem]

Premises used: Part.dom_iff_mem, PFun.Dom
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
⊢ Eq.{u_1 + 1} (α := Set α) (Dom.{u_1, u_2} (β := β) fun (x : α) ↦ { Dom := p x, get := f x }) {x : α | p x}

Tactic:
rfl

Premises used: setOf, PFun.Dom, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
⊢ f.Dom = {x : α | ∃ (y : β), y ∈ f x}

Tactic:
Set.ext (mem_dom f)

Premises used: Set.ext, PFun.mem_dom
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
a : α
⊢ f.fn a = (f a).get

Tactic:
rfl

Premises used: PFun.fn, rfl