awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ (erase x t).size = t.size - 1
have nil : ∀ {a₁ : WithBot α} {a₂ : WithTop α} (h : Valid' a₁ nil a₂) (h_mem : Membership.mem (γ := Ordnode α) nil x),
  (erase x nil).size = size.{u_1} (α := α) nil - 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]
Cleared hypotheses: t, a₁, a₂, h, h_mem
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ (erase x t).size = t.size - 1
have 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₁ (node size t_l t_x t_r) a₂) (h_mem : x ∈ node size t_l t_x t_r),
  (erase x (node size t_l t_x t_r)).size = (node size t_l t_x t_r).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]
Cleared hypotheses: t, a₁, a₂, h, h_mem
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Ordset α
h : s = ∅
⊢ (↑s : Ordnode α).empty = true
have refl : empty.{u_1} (α := α) (↑∅ : Ordnode α) = true
Tactic: cases h
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) s_val property = ∅
have 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 = ∅
Tactic: cases s_val
Cleared hypotheses: s_val, property, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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 = ∅
⊢ Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) s_val property = ∅
have 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 = ∅
Tactic: cases s_val
Cleared hypotheses: s_val, property, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) s_val property = ∅
have 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 = ∅
Tactic: cases s_val <;> [rfl; cases h]
Cleared hypotheses: s_val, property, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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 = ∅
⊢ Subtype.mk (p := fun (t : Ordnode α) ↦ t.Valid) s_val property = ∅
have 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 = ∅
Tactic: cases s_val <;> [rfl; cases h]
Cleared hypotheses: s_val, property, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Ordset α
h : (↑s : Ordnode α).empty = true
⊢ s = ∅
have 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 = ∅
Tactic: cases s with | mk s_val _ => cases s_val <;> [rfl; cases h]
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLE α
x : α
t : Ordset α
h_mem : x ∈ t
⊢ 0 < t.size
have h_mem₁ : Ordnode.mem x (↑t : Ordnode α) = true
Tactic: simp only [Membership.mem, mem, Bool.decide_eq_true] at h_mem
Cleared hypotheses: h_mem
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
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
⊢ { toFun := f₁, invFun := f₂, inv := hf : α ≃. β } = { toFun := f₁, invFun := g₂, inv := hg }
have e_invFun : ∀ (y : β) (x : α), f₂ y = some x ↔ g₂ y = some x
Tactic: congr with y x
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
⊢ 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
have 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
Tactic: simp only [eq_none_iff_forall_not_mem, mem_trans, imp_iff_not_or.symm]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
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
have 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
Tactic: push Not
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
⊢ (PEquiv.refl α).trans f = f
have h : ∀ (x : α) (a : β), ((PEquiv.refl α).trans f : (a : α) → Option β) x = some a ↔ (f : (a : α) → Option β) x = some a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
x : α
a : β
⊢ ((PEquiv.refl α).trans f : (a : α) → Option β) x = some a ↔ (f : (a : α) → Option β) x = some a
have h : (f : (a : α) → Option β) x = some a ↔ (f : (a : α) → Option β) x = some a
Tactic: dsimp [PEquiv.trans]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
⊢ f.trans (PEquiv.refl β) = f
have h : ∀ (x : α) (a : β), (f.trans (PEquiv.refl β) : (a : α) → Option β) x = some a ↔ (f : (a : α) → Option β) x = some a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
x : α
a : β
⊢ (f.trans (PEquiv.refl β) : (a : α) → Option β) x = some a ↔ (f : (a : α) → Option β) x = some a
have h : Option.bind (α := β) ((f : (a : α) → Option β) x) (⇑(PEquiv.refl β) : (a : β) → Option β) = some a ↔
  (f : (a : α) → Option β) x = some a
Tactic: dsimp [PEquiv.trans]
-- Lean 4 proof step from Mathlib.Data.PEquiv (hypothesis)
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
⊢ a₁ = a₂
have h₃ : Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a₁
Tactic: rw [← mem_iff_mem] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Data.PEquiv (hypothesis)
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₁
⊢ a₁ = a₂
have h₄ : Membership.mem (γ := Option α) ((f.symm : (a : β) → Option α) b : Option α) a₂
Tactic: rw [← mem_iff_mem] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
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₂
⊢ a₁ = a₂
have none : ∀ (h : Eq.{u + 1} (α := Option α) ((f.symm : (a : β) → Option α) b : Option α) (none : Option α)), a₁ = a₂
Tactic: cases h : f.symm b
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
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₂
⊢ a₁ = a₂
have some : ∀ (val : α) (h : (f.symm : (a : β) → Option α) b = some val), a₁ = a₂
Tactic: cases h : f.symm b
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome.{v} (α := β) ((f : (a : α) → Option β) a₁) = true
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
have none : ∀ (hfx : Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) x : 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 :
          α))
      none =
    x
Tactic: cases hfx : f x
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
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
⊢ (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
have some : ∀ (val : β) (hfx : (f : (a : α) → Option β) x = 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 :
          α))
      (some val) =
    x
Tactic: cases hfx : f x
-- Lean 4 proof step from Mathlib.Data.PEquiv (hypothesis)
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 β)
⊢ (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
have this : x = a₂
Tactic: have : x = a₂ := not_imp_comm.1 (h x) (hfx.symm ▸ by simp)
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
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 ((f.symm : (a : β) → Option α) val) = x
have some : Option.rec (motive := fun (x : Option α) ↦ α) a₂ id (some x) = x
Tactic: rw [(eq_some_iff f).2 hfx]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → isSome.{v} (α := β) ((f : (a : α) → Option β) a₁) = true
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
have none : ∀ (hfx : Eq.{v + 1} (α := Option β) ((f : (a : α) → Option β) x : 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 :
          α))
      none =
    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
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
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
⊢ (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
have some : ∀ (val : β) (hfx : (f : (a : α) → Option β) x = 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 :
          α))
      (some val) =
    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
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
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 : α
⊢ (if b ∈ s then some b else none) = some a ↔ (if a ∈ s then some a else none) = some b
have pos : ∀ (hb : b ∈ s) (ha : a ∈ s), some b = some a ↔ some a = some b
Tactic: split_ifs with hb ha ha
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
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
⊢ (if b ∈ s then some b else none) = some a ↔ (if a ∈ s then some a else none) = some b
have neg : ∀ (hb : b ∈ s) (ha : ¬a ∈ s), some b = some a ↔ False
Tactic: split_ifs with hb ha ha
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
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
⊢ (if b ∈ s then some b else none) = some a ↔ (if a ∈ s then some a else none) = some b
have pos₁ : ∀ (hb : ¬b ∈ s) (ha : a ∈ s), False ↔ some a = some b
Tactic: split_ifs with hb ha ha
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
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
⊢ (if b ∈ s then some b else none) = some a ↔ (if a ∈ s then some a else none) = some b
have neg₁ : ∀ (hb : ¬b ∈ s) (ha : ¬a ∈ s), False ↔ False
Tactic: split_ifs with hb ha ha
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
⊢ Membership.mem (γ := Option α) ((ofSet s : (a : α) → Option α) a : Option α) a ↔ a ∈ s
have dsimp : (a ∈ if a ∈ s then some a else none) ↔ a ∈ s
Tactic: dsimp [ofSet]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
⊢ (a ∈ if a ∈ s then some a else none) ↔ a ∈ s
have pos : a ∈ s → (a ∈ some a ↔ a ∈ s)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
pos : a ∈ s → (a ∈ some a ↔ a ∈ s)
⊢ (a ∈ if a ∈ s then some a else none) ↔ a ∈ s
have neg : ¬a ∈ s → (Membership.mem (γ := Option α) none a ↔ a ∈ s)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a b : α
⊢ Membership.mem (γ := Option α) ((ofSet s : (a : α) → Option α) b : Option α) a ↔ a = b ∧ a ∈ s
have dsimp : (a ∈ if b ∈ s then some b else none) ↔ a = b ∧ a ∈ s
Tactic: dsimp [ofSet]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
h : ofSet s = PEquiv.refl α
⊢ s = Set.univ
have rw : ∀ (x : α), x ∈ s
Tactic: rw [Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
h : ofSet s = PEquiv.refl α
x : α
⊢ x ∈ s
have rw : Membership.mem (γ := Option α) ((PEquiv.refl α : (a : α) → Option α) x : Option α) x
Tactic: rw [← mem_ofSet_self_iff, h]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
⊢ f.trans f.symm = ofSet {a : α | isSome.{v} (α := β) ((f : (a : α) → Option β) a) = true}
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
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
have 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
Tactic: dsimp [PEquiv.trans]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
f : α ≃. β
x 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
have 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
Tactic: simp only [eq_some_iff f, Option.isSome_iff_exists, bind_eq_some_iff,
    ofSet_eq_some_iff]