awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size t_l t_x t_r) a₂
t_ih_l' : ∀ (h_mem : x ∈ t_l), (erase x t_l).size = t_l.size - 1
t_ih_r' : ∀ (h_mem : x ∈ t_r), (erase x t_r).size = t_r.size - 1
h_mem : true = true
⊢ t_l.size + t_r.size = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size t_l t_x t_r) a₂
t_ih_l' : ∀ (h_mem : x ∈ t_l), (erase x t_l).size = t_l.size - 1
t_ih_r' : ∀ (h_mem : x ∈ t_r), (erase x t_r).size = t_r.size - 1
h_mem : mem x t_r = true
⊢ (erase x t_r).size = t_r.size - 1

Tactic:
have t_ih_r := t_ih_r' h_mem
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
⊢ Valid' (↑t_x : WithBot α) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size

Tactic:
have t_r_h := Valid'.erase_aux x h.right
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_h : Valid' (↑t_x : WithBot α) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
⊢ Valid' (↑t_x : WithBot α) (erase x t_r) a₂

Tactic:
obtain ⟨t_r_valid, t_r_size⟩ := t_r_h
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_h : Valid' (↑t_x : WithBot α) (erase x t_r) a₂ ∧ Raised (erase x t_r).size t_r.size
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
⊢ Raised (erase x t_r).size t_r.size

Tactic:
obtain ⟨t_r_valid, t_r_size⟩ := t_r_h
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
node : t_l.size + (erase x t_r).size + 1 = (Ordnode.node size t_l t_x t_r).size - 1
⊢ (t_l.balanceL t_x (erase x t_r)).size = (Ordnode.node size t_l t_x t_r).size - 1

Tactic:
rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz
          (Or.inr (Exists.intro t_r.size (And.intro t_r_size h.bal.1)))]

Premises used: Ordnode.Valid'.bal, Ordnode.size_balanceL, Ordnode.Valid'.sz, Ordnode.size, And.left, And.intro, Exists.intro, Or.inr, Ordnode.Valid'.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
node : t_l.size + (t_r.size - 1) + 1 = (Ordnode.node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
⊢ t_l.size + (erase x t_r).size + 1 = (Ordnode.node size t_l t_x t_r).size - 1

Tactic:
rw [t_ih_r, h.sz.1]

Premises used: Ordnode.Valid'.sz, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ 0 < t_r.size

Tactic:
have h_pos_t_r_size := pos_size_of_mem h.right.sz h_mem
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_pos_t_r_size : 0 < t_r.size
node :
  ∀ (h_pos_t_r_size : 0 < t_r.size),
    t_l.size + (t_r.size - 1) + 1 = (Ordnode.node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
⊢ t_l.size + (t_r.size - 1) + 1 = (Ordnode.node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
revert h_pos_t_r_size
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
node :
  ∀ (h_pos_t_r_size : LT.lt (α := ℕ) 0 0),
    t_l.size + HSub.hSub (α := ℕ) 0 1 + 1 = (Ordnode.node (t_l.size + 0 + 1) t_l t_x t_r).size - 1
node₁ :
  ∀ (t_r_size : ℕ) (h_pos_t_r_size : 0 < t_r_size + 1),
    t_l.size + (t_r_size + 1 - 1) + 1 = (Ordnode.node (t_l.size + (t_r_size + 1) + 1) t_l t_x t_r).size - 1
⊢ ∀ (h_pos_t_r_size : 0 < t_r.size),
    t_l.size + (t_r.size - 1) + 1 = (Ordnode.node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
rcases t_r.size with - | t_r_size

Premises used: Ordnode.size
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_pos_t_r_size : LT.lt (α := ℕ) 0 0
⊢ t_l.size + HSub.hSub (α := ℕ) 0 1 + 1 = (node (t_l.size + 0 + 1) t_l t_x t_r).size - 1

Tactic:
cases h_pos_t_r_size
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
size : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x : WithBot α) (erase x t_r) a₂
t_r_size_1 : Raised (erase x t_r).size t_r.size
t_r_size : ℕ
h_pos_t_r_size : 0 < t_r_size + 1
⊢ t_l.size + (t_r_size + 1 - 1) + 1 = (node (t_l.size + (t_r_size + 1) + 1) t_l t_x t_r).size - 1

Tactic:
simp [Nat.add_assoc]

Premises used: Nat.add_assoc
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
t : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ t a₂
h_mem : x ∈ t
nil :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ Ordnode.nil a₂)
    (h_mem : Membership.mem (γ := Ordnode α) Ordnode.nil x),
    (erase x Ordnode.nil).size = size.{u_1} (α := α) Ordnode.nil - 1
node :
  ∀ (size : ℕ) (t_l : Ordnode α) (t_x : α) (t_r : Ordnode α)
    (t_ih_l :
      ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ t_l a₂) (h_mem : x ∈ t_l), (erase x t_l).size = t_l.size - 1)
    (t_ih_r :
      ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ t_r a₂) (h_mem : x ∈ t_r), (erase x t_r).size = t_r.size - 1)
    {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ (Ordnode.node size t_l t_x t_r) a₂)
    (h_mem : x ∈ Ordnode.node size t_l t_x t_r),
    (erase x (Ordnode.node size t_l t_x t_r)).size = (Ordnode.node size t_l t_x t_r).size - 1
⊢ (erase x t).size = t.size - 1

Tactic:
induction t generalizing a₁ a₂ with
  | nil =>
    contradiction
  | node _ t_l t_x t_r t_ih_l t_ih_r =>
    have t_ih_l' := t_ih_l h.left
    have t_ih_r' := t_ih_r h.right
    clear t_ih_l t_ih_r
    dsimp only [Membership.mem, mem] at h_mem
    unfold erase
    revert h_mem; cases cmpLE x t_x <;> intro h_mem <;> dsimp only at h_mem ⊢
    · have t_ih_l := t_ih_l' h_mem
      clear t_ih_l' t_ih_r'
      have t_l_h := Valid'.erase_aux x h.left
      obtain ⟨t_l_valid, t_l_size⟩ := t_l_h
      rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz
          (Or.inl (Exists.intro t_l.size (And.intro t_l_size h.bal.1)))]
      rw [t_ih_l, h.sz.1]
      have h_pos_t_l_size := pos_size_of_mem h.left.sz h_mem
      revert h_pos_t_l_size; rcases t_l.size with - | t_l_size <;> intro h_pos_t_l_size
      · cases h_pos_t_l_size
      · simp [Nat.add_right_comm]
    · rw [(Valid'.glue h.left h.right h.bal.1).2, h.sz.1]; rfl
    · have t_ih_r := t_ih_r' h_mem
      clear t_ih_l' t_ih_r'
      have t_r_h := Valid'.erase_aux x h.right
      obtain ⟨t_r_valid, t_r_size⟩ := t_r_h
      rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz
          (Or.inr (Exists.intro t_r.size (And.intro t_r_size h.bal.1)))]
      rw [t_ih_r, h.sz.1]
      have h_pos_t_r_size := pos_size_of_mem h.right.sz h_mem
      revert h_pos_t_r_size; rcases t_r.size with - | t_r_size <;> intro h_pos_t_r_size
      · cases h_pos_t_r_size
      · simp [Nat.add_assoc]

Premises used: Membership.mem, Ordnode.mem, Ordnode.erase, Ordnode.node, Ordnode.nil, Nat.add_assoc, Nat.add_right_comm
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
s : Ordset α
h : s = ∅
refl : empty.{u_1} (α := α) (↑∅ : Ordnode α) = true
⊢ (↑s : Ordnode α).empty = true

Tactic:
cases h
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
⊢ empty.{u_1} (α := α) (↑∅ : Ordnode α) = true

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
⊢ empty.{u_1} (α := α) (↑∅ : Ordnode α) = true

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
s_val : Ordnode α
property : s_val.Valid
h : (↑(Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) s_val property) : Ordnode α).empty = true
mk :
  ∀ (property : Valid.{u_1} (α := α) Ordnode.nil)
    (h : (↑(Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) Ordnode.nil property) : Ordnode α).empty = true),
    Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) Ordnode.nil property = ∅
mk₁ :
  ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (property : (node size l x r).Valid)
    (h : (↑(Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) (node size l x r) property) : Ordnode α).empty = true),
    Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) (node size l x r) property = ∅
⊢ Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) s_val property = ∅

Tactic:
cases s_val
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
property : Valid.{u_1} (α := α) Ordnode.nil
h : (↑(Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) Ordnode.nil property) : Ordnode α).empty = true
⊢ Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) Ordnode.nil property = ∅

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
property : (node size l x r).Valid
h : (↑(Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) (node size l x r) property) : Ordnode α).empty = true
⊢ Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) (node size l x r) property = ∅

Tactic:
cases h
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
s_val : Ordnode α
property : s_val.Valid
h : (↑(Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) s_val property) : Ordnode α).empty = true
mk :
  ∀ (property : Valid.{u_1} (α := α) Ordnode.nil)
    (h : (↑(Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) Ordnode.nil property) : Ordnode α).empty = true),
    Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) Ordnode.nil property = ∅
mk₁ :
  ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (property : (node size l x r).Valid)
    (h : (↑(Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) (node size l x r) property) : Ordnode α).empty = true),
    Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) (node size l x r) property = ∅
mk₂ :
  ∀ (property : Valid.{u_1} (α := α) Ordnode.nil)
    (h : (↑(Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) Ordnode.nil property) : Ordnode α).empty = true),
    Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) Ordnode.nil property = ∅
mk₃ :
  ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (property : (node size l x r).Valid)
    (h : (↑(Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) (node size l x r) property) : Ordnode α).empty = true),
    Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) (node size l x r) property = ∅
⊢ Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) s_val property = ∅

Tactic:
cases s_val <;> [rfl; cases h]
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
s : Ordset α
h : (↑s : Ordnode α).empty = true
mk :
  ∀ (s_val : Ordnode α) (property : s_val.Valid)
    (h : (↑(Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) s_val property) : Ordnode α).empty = true),
    Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) s_val property = ∅
⊢ s = ∅

Tactic:
cases s with | mk s_val _ => cases s_val <;> [rfl; cases h]
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
t : Ordset α
h_mem : x ∈ t
⊢ Ordnode.mem x (↑t : Ordnode α) = true

Tactic:
simp only [Membership.mem, mem, Bool.decide_eq_true] at h_mem

Premises used: Membership.mem, Bool.decide_eq_true, Ordset.mem
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
t : Ordset α
h_mem : Ordnode.mem x (↑t : Ordnode α) = true
⊢ 0 < t.size

Tactic:
apply Ordnode.pos_size_of_mem t.property.sz h_mem

Premises used: Ordnode.Valid'.sz, Ordnode.pos_size_of_mem, Subtype.property
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
f₁ : α → Option β
f₂ : β → Option α
hf : ∀ (a : α) (b : β), f₂ b = some a ↔ f₁ a = some b
g₂ : β → Option α
hg : ∀ (a : α) (b : β), g₂ b = some a ↔ f₁ a = some b
e_invFun : ∀ (y : β) (x : α), f₂ y = some x ↔ g₂ y = some x
⊢ { toFun := f₁, invFun := f₂, inv := hf : α ≃. β } = { toFun := f₁, invFun := g₂, inv := hg }

Tactic:
congr with y x
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
f₁ : α → Option β
f₂ : β → Option α
hf : ∀ (a : α) (b : β), f₂ b = some a ↔ f₁ a = some b
g₂ : β → Option α
hg : ∀ (a : α) (b : β), g₂ b = some a ↔ f₁ a = some b
y : β
x : α
⊢ f₂ y = some x ↔ g₂ y = some x

Tactic:
simp only [hf, hg]
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f₁ : α → Option β
f₂ : β → Option α
h : ∀ (a : α) (b : β), f₂ b = some a ↔ f₁ a = some b
⊢ (⇑{ toFun := f₁, invFun := f₂, inv := h : α ≃. β } : (a : α) → Option β) = f₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f₁ : α → Option β
f₂ : β → Option α
h : ∀ (a : α) (b : β), f₂ b = some a ↔ f₁ a = some b
x : α
⊢ ({ toFun := f₁, invFun := f₂, inv := h : α ≃. β } : (a : α) → Option β) x = f₁ x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f g : α ≃. β
h :
  ∀ (x : α), Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) x : Option β) ((g : (a : α) → Option β) x : Option β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a : α
b : β
⊢ Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a ↔
    Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b

Tactic:
f.3 _ _

Premises used: PEquiv.inv
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a : α
b : β
⊢ (f.symm : (a : β) → Option α) b = some a ↔ (f : (a : α) → Option β) a = some b

Tactic:
f.3 _ _

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

Tactic:
simp_all [and_comm, eq_some_iff f, eq_some_iff g, bind_eq_some_iff]

Premises used: and_comm, PEquiv.eq_some_iff, Option.bind_eq_some_iff
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
a : α
⊢ (PEquiv.refl α : (a : α) → Option α) a = some a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
⊢ (PEquiv.refl α).symm = PEquiv.refl α

Tactic:
rfl

Premises used: PEquiv.refl, rfl
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
⊢ f.symm.symm = f

Tactic:
rfl

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

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, PEquiv.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
⊢ Injective (α := α ≃. β) PEquiv.symm

Tactic:
symm_bijective.injective

Premises used: Function.Bijective.injective, PEquiv.symm_bijective
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
g : β ≃. γ
h : γ ≃. δ
⊢ (f.trans g).trans h = f.trans (g.trans h)

Tactic:
ext fun _ => Option.bind_assoc _ _ _

Premises used: Option.bind_assoc, DFunLike.coe, PEquiv.ext
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
c : γ
⊢ Membership.mem (γ := Option γ) ((f.trans g : (a : α) → Option γ) a : Option γ) c ↔
    ∃ (b : β),
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b ∧
        Membership.mem (γ := Option γ) ((g : (a : β) → Option γ) b : Option γ) c

Tactic:
Option.bind_eq_some_iff

Premises used: Option.bind_eq_some_iff
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
c : γ
⊢ (f.trans g : (a : α) → Option γ) a = some c ↔
    ∃ (b : β), (f : (a : α) → Option β) a = some b ∧ (g : (a : β) → Option γ) b = some c

Tactic:
Option.bind_eq_some_iff

Premises used: Option.bind_eq_some_iff
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
simp :
  (∀ (a_1 : γ),
      ¬∃ (b : β),
          Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b ∧
            Membership.mem (γ := Option γ) ((g : (a : β) → Option γ) b : Option γ) a_1) ↔
    ∀ (b : β) (c : γ),
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b →
        ¬Membership.mem (γ := Option γ) ((g : (a : β) → Option γ) b : Option γ) c
⊢ Eq.{w + 1} (α := Option γ) ((f.trans g : (a : α) → Option γ) a : Option γ) (none : Option γ) ↔
    ∀ (b : β) (c : γ),
      ¬Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b ∨
        ¬Membership.mem (γ := Option γ) ((g : (a : β) → Option γ) b : Option γ) c

Tactic:
simp only [eq_none_iff_forall_not_mem, mem_trans, imp_iff_not_or.symm]

Premises used: imp_iff_not_or, PEquiv.mem_trans, Option.eq_none_iff_forall_not_mem, Iff.symm
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
push :
  (∀ (a_1 : γ) (b : β) (_ : Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b),
      ¬Membership.mem (γ := Option γ) ((g : (a : β) → Option γ) b : Option γ) a_1) ↔
    ∀ (b : β) (c : γ),
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b →
        ¬Membership.mem (γ := Option γ) ((g : (a : β) → Option γ) b : Option γ) c
⊢ (∀ (a_1 : γ),
      ¬∃ (b : β),
          Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b ∧
            Membership.mem (γ := Option γ) ((g : (a : β) → Option γ) b : Option γ) a_1) ↔
    ∀ (b : β) (c : γ),
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b →
        ¬Membership.mem (γ := Option γ) ((g : (a : β) → Option γ) b : Option γ) c

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ) (b : β) (_ : Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b),
      ¬Membership.mem (γ := Option γ) ((g : (a : β) → Option γ) b : Option γ) a_1) ↔
    ∀ (b : β) (c : γ),
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b →
        ¬Membership.mem (γ := Option γ) ((g : (a : β) → Option γ) b : Option γ) c

Tactic:
forall_comm

Premises used: forall_comm
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ) (b : β) (_ : Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b),
      ¬Membership.mem (γ := Option γ) ((g : (a : β) → Option γ) b : Option γ) a_1) ↔
    ∀ (b : β) (c : γ),
      Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b →
        ¬Membership.mem (γ := Option γ) ((g : (a : β) → Option γ) b : Option γ) c

Tactic:
exact forall_comm

Premises used: forall_comm
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
h : ∀ (x : α) (a : β), ((PEquiv.refl α).trans f : (a : α) → Option β) x = some a ↔ (f : (a : α) → Option β) x = some a
⊢ (PEquiv.refl α).trans f = f

Tactic:
ext
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
x : α
a : β
h : (f : (a : α) → Option β) x = some a ↔ (f : (a : α) → Option β) x = some a
⊢ ((PEquiv.refl α).trans f : (a : α) → Option β) x = some a ↔ (f : (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 : β
⊢ (f : (a : α) → Option β) x = some a ↔ (f : (a : α) → Option β) x = some a

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

Tactic:
ext
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
x : α
a : β
h :
  Option.bind (α := β) ((f : (a : α) → Option β) x) (⇑(PEquiv.refl β) : (a : β) → Option β) = some a ↔
    (f : (a : α) → Option β) x = some a
⊢ (f.trans (PEquiv.refl β) : (a : α) → Option β) x = some a ↔ (f : (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 : β
⊢ Option.bind (α := β) ((f : (a : α) → Option β) x) (⇑(PEquiv.refl β) : (a : β) → Option β) = some a ↔
    (f : (a : α) → Option β) x = some a

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

Tactic:
rw [← mem_iff_mem] at *

Premises used: PEquiv.mem_iff_mem
-- Module: Mathlib.Data.PEquiv
Goal:
α : Type u
β : Type v
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : Membership.mem (γ := Option β) ((f : (a : α) → Option β) a₁ : Option β) b
h₂ : Membership.mem (γ := Option β) ((f : (a : α) → Option β) a₂ : Option β) b
h₃ : Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a₁
⊢ Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a₂

Tactic:
rw [← mem_iff_mem] at *

Premises used: PEquiv.mem_iff_mem
-- 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₂
none : ∀ (h : Eq.{u + 1} (α := Option α) ((f.symm : (a : β) → Option α) b : Option α) (Option.none : Option α)), a₁ = a₂
some : ∀ (val : α) (h : (f.symm : (a : β) → Option α) b = Option.some val), a₁ = a₂
⊢ a₁ = a₂

Tactic:
cases h : f.symm b

Premises used: DFunLike.coe, PEquiv.symm