awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.Nat (goal)
Goal:
h :
  ∀ (x : ℕ),
    Eq (α := ℕ) ((natSumNatEquivNat : (a : ℕ ⊕ ℕ) → ℕ) (Sum.inl x) : ℕ)
      (Sum.elim (fun (x : ℕ) ↦ 2 * x) (fun (x : ℕ) ↦ 2 * x + 1) (Sum.inl x) : ℕ)
⊢ Eq (α := (a : ℕ ⊕ ℕ) → ℕ) (⇑natSumNatEquivNat : (a : ℕ ⊕ ℕ) → ℕ)
    (Sum.elim (fun (x : ℕ) ↦ 2 * x) fun (x : ℕ) ↦ 2 * x + 1)
have h₁ : ∀ (x : ℕ),
  Eq (α := ℕ) ((natSumNatEquivNat : (a : ℕ ⊕ ℕ) → ℕ) (Sum.inr x) : ℕ)
    (Sum.elim (fun (x : ℕ) ↦ 2 * x) (fun (x : ℕ) ↦ 2 * x + 1) (Sum.inr x) : ℕ)
Tactic: ext (x | x)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
⊢ (e₁.trans e₂).optionCongr = e₁.optionCongr.trans e₂.optionCongr
have H : ∀ (x : Option α),
  Eq.{u_3 + 1} (α := Option γ) (((e₁.trans e₂).optionCongr : (a : Option α) → Option γ) x : Option γ)
    ((e₁.optionCongr.trans e₂.optionCongr : (a : Option α) → Option γ) x : Option γ)
Tactic: ext x : 1
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
x : Option α
⊢ Eq.{u_3 + 1} (α := Option γ) (((e₁.trans e₂).optionCongr : (a : Option α) → Option γ) x : Option γ)
    ((e₁.optionCongr.trans e₂.optionCongr : (a : Option α) → Option γ) x : Option γ)
have H : Eq.{u_3 + 1} (α := Option γ) ((e₁.optionCongr.trans e₂.optionCongr : (a : Option α) → Option γ) x : Option γ)
  (((e₁.trans e₂).optionCongr : (a : Option α) → Option γ) x : Option γ)
Tactic: symm
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h : ¬isSome.{u_2} (α := β) ((e : (a : Option α) → Option β) (some x)) = true
⊢ isSome.{u_2} (α := β) ((e : (a : Option α) → Option β) none) = true
have rw : Ne.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) none : Option β) (none : Option β)
Tactic: rw [← Option.ne_none_iff_isSome]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h : ¬isSome.{u_2} (α := β) ((e : (a : Option α) → Option β) (some x)) = true
hn : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) none : Option β) (none : Option β)
⊢ False
have h₁ : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β)
  ((e : (a : Option α) → Option β) none : Option β)
Tactic: rw [Option.not_isSome_iff_eq_none, ← hn] at h
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
have none : ∀
  (h1 :
    Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) : Option α)
      (none : Option α)),
  some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
Tactic: cases h1 : e.symm (some (removeNone_aux e x))
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
none :
  ∀
    (h1 :
      Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) : Option α)
        (Option.none : Option α)),
    some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
have some : ∀ (val : α) (h1 : (e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) = some val),
  some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
Tactic: cases h1 : e.symm (some (removeNone_aux e x))
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h1 :
  Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) : Option α)
    (none : Option α)
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
have none : ∀ (h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)),
  some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
Tactic: cases h2 : e (some x)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h1 :
  Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) : Option α)
    (Option.none : Option α)
none :
  ∀ (h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (Option.none : Option β)),
    some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
have none₁ : ∀ (val : β) (h2 : (e : (a : Option α) → Option β) (some x) = some val),
  some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
Tactic: cases h2 : e (some x)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x val : α
h1 : (e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) = some val
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
have some : ∀ (h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)),
  some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
Tactic: cases h2 : e (some x)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x val : α
h1 : (e.symm : (a : Option β) → Option α) (Option.some (e.removeNone_aux x)) = Option.some val
some :
  ∀ (h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (Option.some x) : Option β) (none : Option β)),
    Option.some (e.symm.removeNone_aux (e.removeNone_aux x)) = Option.some x
⊢ Option.some (e.symm.removeNone_aux (e.removeNone_aux x)) = Option.some x
have some₁ : ∀ (val : β) (h2 : (e : (a : Option α) → Option β) (Option.some x) = Option.some val),
  Option.some (e.symm.removeNone_aux (e.removeNone_aux x)) = Option.some x
Tactic: cases h2 : e (some x)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h1 :
  Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) : Option α)
    (none : Option α)
h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
have none : (e.symm : (a : Option β) → Option α) none = some x
Tactic: rw [removeNone_aux_none _ h1]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h1 :
  Eq.{u_1 + 1} (α := Option α) ((e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) : Option α)
    (none : Option α)
val : β
h2 : (e : (a : Option α) → Option β) (some x) = some val
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
have none : ∀
  (h1 :
    Eq.{u_1 + 1} (α := Option α)
      ((e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) (some x)) : Option α) (none : Option α))
  (val : β) (h2 : (e : (a : Option α) → Option β) (some x) = some val),
  some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
Tactic: rw [removeNone_aux_some _ ⟨_, h2⟩] at h1
Cleared hypotheses: h1, val, h2
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (hypothesis)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x val : α
h1 : (e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) = some val
h2 : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
have h1₁ : (e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) none) = some val
Tactic: rw [removeNone_aux_none _ h2] at h1
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x val : α
h1 : (e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) = some val
val_1 : β
h2 : (e : (a : Option α) → Option β) (some x) = some val_1
⊢ some (e.symm.removeNone_aux (e.removeNone_aux x)) = some x
have some : (e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) = some x
Tactic: rw [removeNone_aux_some _ ⟨_, h1⟩]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x val : α
h1 : (e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) = some val
val_1 : β
h2 : (e : (a : Option α) → Option β) (some x) = some val_1
⊢ (e.symm : (a : Option β) → Option α) (some (e.removeNone_aux x)) = some x
have some : (e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) (some x)) = some x
Tactic: rw [removeNone_aux_some _ ⟨_, h2⟩]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
⊢ Eq.{u_2 + 1} (α := Option β) (some ((e.removeNone : (a : α) → β) x) : Option β)
      ((e : (a : Option α) → Option β) none : Option β) ↔
    (e.symm : (a : Option β) → Option α) none = some x
have none : ∀ (h : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)),
  Eq.{u_2 + 1} (α := Option β) (some ((e.removeNone : (a : α) → β) x) : Option β)
      ((e : (a : Option α) → Option β) none : Option β) ↔
    (e.symm : (a : Option β) → Option α) none = some x
Tactic: rcases h : e (some x) with a | a
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
none :
  ∀ (h : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (Option.none : Option β)),
    Eq.{u_2 + 1} (α := Option β) (some ((e.removeNone : (a : α) → β) x) : Option β)
        ((e : (a : Option α) → Option β) Option.none : Option β) ↔
      (e.symm : (a : Option β) → Option α) Option.none = some x
⊢ Eq.{u_2 + 1} (α := Option β) (some ((e.removeNone : (a : α) → β) x) : Option β)
      ((e : (a : Option α) → Option β) Option.none : Option β) ↔
    (e.symm : (a : Option β) → Option α) Option.none = some x
have some : ∀ (a : β) (h : (e : (a : Option α) → Option β) (some x) = some a),
  Eq.{u_2 + 1} (α := Option β) (some ((e.removeNone : (a : α) → β) x) : Option β)
      ((e : (a : Option α) → Option β) Option.none : Option β) ↔
    (e.symm : (a : Option β) → Option α) Option.none = some x
Tactic: rcases h : e (some x) with a | a
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
h : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β) (none : Option β)
⊢ Eq.{u_2 + 1} (α := Option β) (some ((e.removeNone : (a : α) → β) x) : Option β)
      ((e : (a : Option α) → Option β) none : Option β) ↔
    (e.symm : (a : Option β) → Option α) none = some x
have none : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) none : Option β)
    ((e : (a : Option α) → Option β) none : Option β) ↔
  (e.symm : (a : Option β) → Option α) none = some x
Tactic: rw [removeNone_none _ h]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
a : β
h : (e : (a : Option α) → Option β) (some x) = some a
⊢ Eq.{u_2 + 1} (α := Option β) (some ((e.removeNone : (a : α) → β) x) : Option β)
      ((e : (a : Option α) → Option β) none : Option β) ↔
    (e.symm : (a : Option β) → Option α) none = some x
have some : Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β)
    ((e : (a : Option α) → Option β) none : Option β) ↔
  (e.symm : (a : Option β) → Option α) none = some x
Tactic: rw [removeNone_some _ ⟨a, h⟩]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (hypothesis)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
a : β
h : (e : (a : Option α) → Option β) (some x) = some a
⊢ Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β)
      ((e : (a : Option α) → Option β) none : Option β) ↔
    (e.symm : (a : Option β) → Option α) none = some x
have h1 : Eq.{u_1 + 1} (α := Option α)
  ((e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) (some x)) : Option α)
  ((e.symm : (a : Option β) → Option α) (some a) : Option α)
Tactic: have h1 := congr_arg e.symm h
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (hypothesis)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
a : β
h : (e : (a : Option α) → Option β) (some x) = some a
h1 :
  Eq.{u_1 + 1} (α := Option α)
    ((e.symm : (a : Option β) → Option α) ((e : (a : Option α) → Option β) (some x)) : Option α)
    ((e.symm : (a : Option β) → Option α) (some a) : Option α)
⊢ Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β)
      ((e : (a : Option α) → Option β) none : Option β) ↔
    (e.symm : (a : Option β) → Option α) none = some x
have h1₁ : some x = (e.symm : (a : Option β) → Option α) (some a)
Tactic: rw [symm_apply_apply] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
e : Equiv.{u_1 + 1, u_2 + 1} (Option α) (Option β)
x : α
a : β
h : (e : (a : Option α) → Option β) (some x) = some a
h1 : some x = (e.symm : (a : Option β) → Option α) (some a)
⊢ Eq.{u_2 + 1} (α := Option β) ((e : (a : Option α) → Option β) (some x) : Option β)
      ((e : (a : Option α) → Option β) none : Option β) ↔
    (e.symm : (a : Option β) → Option α) none = some x
have some : False ↔ (e.symm : (a : Option β) → Option α) none = some x
Tactic: simp only [apply_eq_iff_eq, reduceCtorEq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }
a : α
⊢ (fun (b : { y : β // y ≠ x }) ↦ Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) ⋯)
      ((fun (a : α) ↦
          (Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯ :
            { y : β // y ≠ x }))
        a) =
    a
have rw : ((↑e : Option α ≃ β).symm : (a : β) → Option α)
    (↑((fun (a : α) ↦
            (Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) sorry :
              { y : β // y ≠ x }))
          a) :
      β) =
  some a
Tactic: rw [← some_inj, some_get]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : { e : Equiv.{u_1 + 1, u_2 + 1} (Option α) β // (e : (a : Option α) → β) none = x }
b : { y : β // y ≠ x }
⊢ (fun (a : α) ↦
        (Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) ⋯ :
          { y : β // y ≠ x }))
      ((fun (b : { y : β // y ≠ x }) ↦ Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) ⋯) b) =
    b
have a : (↑((fun (a : α) ↦
          (Subtype.mk (p := fun (y : β) ↦ y ≠ x) (((↑e : Option α ≃ β) : (a : Option α) → β) (some a)) sorry :
            { y : β // y ≠ x }))
        ((fun (b : { y : β // y ≠ x }) ↦ Option.get (((↑e : Option α ≃ β).symm : (a : β) → Option α) (↑b : β)) sorry) b)) :
    β) =
  (↑b : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
a : α
⊢ (fun (b : β) ↦
        (if h : b = x then none
          else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
          Option α))
      ((fun (a : Option α) ↦
          a.casesOn' x
            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
              (⇑e : (a : α) → { y : β // y ≠ x })))
        (some a)) =
    some a
have some : (if (↑((e : (a : α) → { y : β // y ≠ x }) a) : β) = x then none else some a) = some a
Tactic: simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta,
              symm_apply_apply, dite_eq_ite]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
a : Option α
⊢ (fun (b : β) ↦
        (if h : b = x then none
          else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
          Option α))
      ((fun (a : Option α) ↦
          a.casesOn' x
            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
              (⇑e : (a : α) → { y : β // y ≠ x })))
        a) =
    a
have none : Eq.{u_1 + 1} (α := Option α)
  ((fun (b : β) ↦
      (if h : b = x then none
        else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
        Option α))
    ((fun (a : Option α) ↦
        a.casesOn' x
          (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
            (⇑e : (a : α) → { y : β // y ≠ x })))
      none))
  none
Tactic: cases a with
          | none => simp
          | some a =>
            simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta,
              symm_apply_apply, dite_eq_ite]
            exact if_neg (e a).property
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
a : Option α
none :
  Eq.{u_1 + 1} (α := Option α)
    ((fun (b : β) ↦
        (if h : b = x then Option.none
          else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
          Option α))
      ((fun (a : Option α) ↦
          a.casesOn' x
            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
              (⇑e : (a : α) → { y : β // y ≠ x })))
        Option.none))
    Option.none
⊢ (fun (b : β) ↦
        (if h : b = x then Option.none
          else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
          Option α))
      ((fun (a : Option α) ↦
          a.casesOn' x
            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
              (⇑e : (a : α) → { y : β // y ≠ x })))
        a) =
    a
have some : ∀ (a : α),
  (fun (b : β) ↦
        (if h : b = x then Option.none
          else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
          Option α))
      ((fun (a : Option α) ↦
          a.casesOn' x
            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
              (⇑e : (a : α) → { y : β // y ≠ x })))
        (some a)) =
    some a
Tactic: cases a with
          | none => simp
          | some a =>
            simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta,
              symm_apply_apply, dite_eq_ite]
            exact if_neg (e a).property
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
b : β
⊢ (fun (a : Option α) ↦
        a.casesOn' x
          (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
            (⇑e : (a : α) → { y : β // y ≠ x })))
      ((fun (b : β) ↦
          (if h : b = x then none
            else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
            Option α))
        b) =
    b
have pos : ∀ (h : b = x),
  (fun (a : Option α) ↦
        a.casesOn' x
          (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
            (⇑e : (a : α) → { y : β // y ≠ x })))
      ((fun (b : β) ↦
          (if h : b = x then none
            else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
            Option α))
        b) =
    b
Tactic: by_cases h : b = x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Option (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
x : β
e : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α { y : β // y ≠ x }
b : β
pos :
  ∀ (h : b = x),
    (fun (a : Option α) ↦
          a.casesOn' x
            (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
              (⇑e : (a : α) → { y : β // y ≠ x })))
        ((fun (b : β) ↦
            (if h : b = x then none
              else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
              Option α))
          b) =
      b
⊢ (fun (a : Option α) ↦
        a.casesOn' x
          (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
            (⇑e : (a : α) → { y : β // y ≠ x })))
      ((fun (b : β) ↦
          (if h : b = x then none
            else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
            Option α))
        b) =
    b
have neg : ∀ (h : ¬b = x),
  (fun (a : Option α) ↦
        a.casesOn' x
          (Function.comp (β := { y : β // y ≠ x }) (Subtype.val (p := fun (y : β) ↦ y ≠ x))
            (⇑e : (a : α) → { y : β // y ≠ x })))
      ((fun (b : β) ↦
          (if h : b = x then none
            else some ((e.symm : (a : { y : β // y ≠ x }) → α) (Subtype.mk (p := fun (y : β) ↦ y ≠ x) b h)) :
            Option α))
        b) =
    b
Tactic: by_cases h : b = x