awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
rw rw₁ :
  -[(↑n.pred' : ℕ) / HAdd.hAdd (α := ℕ) (↑d.pred' : ℕ) 1+1] = -[(↑n.pred' : ℕ) / HAdd.hAdd (α := ℕ) (↑d.pred' : ℕ) 1+1]
⊢ -[HDiv.hDiv (α := ℕ) (↑n.pred' : ℕ) (↑d : ℕ)+1] = -[(↑n.pred' : ℕ) / HAdd.hAdd (α := ℕ) (↑d.pred' : ℕ) 1+1]

Tactic:
rw [d.to_nat_eq_succ_pred]

Premises used: PosNum.to_nat_eq_succ_pred
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
rw :
  (↑(HDiv.hDiv (α := ℕ) (↑n.pred' : ℕ) (↑(Num.pos d) : ℕ) + 1) : ℤ) =
    -HAdd.hAdd (α := ℤ) (↑(↑n.pred' : ℕ) : ℤ) 1 / -HAdd.hAdd (α := ℤ) (↑(↑d.pred' : ℕ) : ℤ) 1
⊢ (↑(n.pred' / Num.pos d).succ' : ℤ) = HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (-(↑d : ℤ))

Tactic:
rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred, ← PosNum.to_nat_to_int, Num.succ'_to_nat,
        Num.div_to_nat]

Premises used: Num.div_to_nat, Num.succ'_to_nat, PosNum.to_int_eq_succ_pred, PosNum.to_nat_to_int
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
rw rw₁ :
  Eq (α := ℤ) (↑((↑n.pred' : ℕ) / HAdd.hAdd (α := ℕ) (↑d.pred' : ℕ) 1).succ : ℤ)
    (↑((↑n.pred' : ℕ) / HAdd.hAdd (α := ℕ) (↑d.pred' : ℕ) 1).succ : ℤ)
⊢ Eq (α := ℤ) (↑(HDiv.hDiv (α := ℕ) (↑n.pred' : ℕ) (↑d : ℕ)).succ : ℤ)
    (↑((↑n.pred' : ℕ) / HAdd.hAdd (α := ℕ) (↑d.pred' : ℕ) 1).succ : ℤ)

Tactic:
rw [d.to_nat_eq_succ_pred]

Premises used: PosNum.to_nat_eq_succ_pred
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : PosNum
d : ZNum
rw : (↑((↑(Num.pos n) : ℕ) % natAbs (↑d : ℤ)) : ℤ) = HMod.hMod (α := ℤ) (↑(↑n : ℕ) : ℤ) (↑d : ℤ)
⊢ (↑(Num.pos n % d.abs) : ℤ) = HMod.hMod (α := ℤ) (↑(pos n) : ℤ) (↑d : ℤ)

Tactic:
rw [← Num.to_nat_to_int, cast_pos, Num.mod_to_nat, ← PosNum.to_nat_to_int, abs_to_nat]

Premises used: ZNum.abs_to_nat, ZNum.cast_pos, Num.to_nat_to_int, PosNum.to_nat_to_int, Num.mod_to_nat
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : PosNum
d : ZNum
⊢ (↑((↑(Num.pos n) : ℕ) % natAbs (↑d : ℤ)) : ℤ) = HMod.hMod (α := ℤ) (↑(↑n : ℕ) : ℤ) (↑d : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : PosNum
d : ZNum
rw :
  subNatNat (natAbs (↑d : ℤ)) ((↑n.pred' : ℕ) % natAbs (↑d : ℤ) + 1) =
    -HAdd.hAdd (α := ℤ) (↑(↑n.pred' : ℕ) : ℤ) 1 % (↑d : ℤ)
⊢ HSub.hSub (α := ℤ) (↑d.abs : ℤ) (↑(n.pred' % d.abs).succ : ℤ) = HMod.hMod (α := ℤ) (↑(neg n) : ℤ) (↑d : ℤ)

Tactic:
rw [← Num.to_nat_to_int, cast_neg, ← Num.to_nat_to_int, Num.succ_to_nat, Num.mod_to_nat,
          abs_to_nat, ← Int.subNatNat_eq_coe, n.to_int_eq_succ_pred]

Premises used: ZNum.cast_neg, Num.succ_to_nat, PosNum.to_int_eq_succ_pred, ZNum.abs_to_nat, Int.subNatNat_eq_coe, Num.to_nat_to_int, Num.mod_to_nat
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : PosNum
d : ZNum
⊢ subNatNat (natAbs (↑d : ℤ)) ((↑n.pred' : ℕ) % natAbs (↑d : ℤ) + 1) =
    -HAdd.hAdd (α := ℤ) (↑(↑n.pred' : ℕ) : ℤ) 1 % (↑d : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : ZNum
simp : (natAbs (↑a : ℤ)).gcd (natAbs (↑b : ℤ)) = Int.gcd (↑a : ℤ) (↑b : ℤ)
⊢ Nat.gcd (↑a.abs : ℕ) (↑b.abs : ℕ) = Int.gcd (↑a : ℤ) (↑b : ℤ)

Tactic:
simp only [abs_to_nat]

Premises used: ZNum.abs_to_nat
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : ZNum
⊢ (natAbs (↑a : ℤ)).gcd (natAbs (↑b : ℤ)) = Int.gcd (↑a : ℤ) (↑b : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
m n : ZNum
rw : HMod.hMod (α := ℤ) (↑n : ℤ) (↑m : ℤ) = 0 ↔ HMod.hMod (α := ℤ) (↑n : ℤ) (↑m : ℤ) = (↑0 : ℤ)
⊢ m ∣ n ↔ n % m = 0

Tactic:
rw [← dvd_to_int, Int.dvd_iff_emod_eq_zero, ← to_int_inj, mod_to_int]

Premises used: ZNum.mod_to_int, ZNum.dvd_to_int, ZNum.to_int_inj, Int.dvd_iff_emod_eq_zero
-- Module: Mathlib.Data.Num.ZNum
Goal:
m n : ZNum
⊢ HMod.hMod (α := ℤ) (↑n : ℤ) (↑m : ℤ) = 0 ↔ HMod.hMod (α := ℤ) (↑n : ℤ) (↑m : ℤ) = (↑0 : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
⊢ Function.Injective.{u, max 1 u} (α := α) op

Tactic:
fun _ _ => congr_arg Opposite.unop

Premises used: congr_arg, Function.Injective, Opposite.unop
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
⊢ Function.Injective.{max 1 u, u} (α := αᵒᵖ) unop

Tactic:
fun _ _ h => congrArg op h

Premises used: congrArg, Opposite.op, Function.Injective
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
x : αᵒᵖ
⊢ Eq.{max 1 u} (op (unop x)) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
x : α
⊢ unop (op x) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
x y : α
⊢ Eq.{max 1 u} (op x) (op y) ↔ x = y

Tactic:
op_injective.eq_iff

Premises used: Function.Injective.eq_iff, Opposite.op_injective
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
x y : αᵒᵖ
⊢ unop x = unop y ↔ Eq.{max 1 u} x y

Tactic:
unop_injective.eq_iff

Premises used: Function.Injective.eq_iff, Opposite.unop_injective
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
⊢ Function.Surjective.{u, max 1 u} (α := α) op

Tactic:
equivToOpposite.surjective

Premises used: Opposite.equivToOpposite, Equiv.surjective
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
⊢ Function.Surjective.{max 1 u, u} (α := αᵒᵖ) unop

Tactic:
equivToOpposite.symm.surjective

Premises used: Opposite.equivToOpposite, Equiv.surjective, Equiv.symm
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
⊢ Eq.{max 1 u} (α := (a : α) → αᵒᵖ) (⇑equivToOpposite : (a : α) → αᵒᵖ) op

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
⊢ Eq (α := (a : αᵒᵖ) → α) (⇑(Equiv.symm equivToOpposite) : (a : αᵒᵖ) → α) unop

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
x : α
y : αᵒᵖ
⊢ Eq.{max 1 u} (op x) y ↔ x = unop y

Tactic:
equivToOpposite.apply_eq_iff_eq_symm_apply

Premises used: Opposite.equivToOpposite, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
x : αᵒᵖ
y : α
⊢ unop x = y ↔ Eq.{max 1 u} x (op y)

Tactic:
equivToOpposite.symm.apply_eq_iff_eq_symm_apply

Premises used: Opposite.equivToOpposite, Equiv.symm, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
inst : Nonempty α
⊢ Nonempty.{max 1 u} αᵒᵖ

Tactic:
Nonempty.map op ‹_›

Premises used: Opposite.op, Nonempty.map
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
inst : Subsingleton α
⊢ Subsingleton.{max 1 u} αᵒᵖ

Tactic:
unop_injective.subsingleton

Premises used: Function.Injective.subsingleton, Opposite.unop_injective
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
X : Type v
inst : Small.{u, v} X
obtain : ∀ (S : Type u) (e : X ≃ S), Small.{u, v} Xᵒᵖ
⊢ Small.{u, v} Xᵒᵖ

Tactic:
obtain ⟨S, ⟨e⟩⟩ := Small.equiv_small (α := X)

Premises used: Small.equiv_small
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
X : Type v
inst : Small.{u, v} X
S : Type u
e : X ≃ S
⊢ Small.{u, v} Xᵒᵖ

Tactic:
⟨S, ⟨equivToOpposite.symm.trans e⟩⟩

Premises used: Equiv.trans, Opposite.equivToOpposite, Small.mk, Nonempty.intro, Exists.intro, Equiv.symm
-- Module: Mathlib.Data.Opposite
Goal:
α : Sort u
X : Type v
inst : Small.{u, v} X
S : Type u
e : X ≃ S
⊢ Small.{u, v} Xᵒᵖ

Tactic:
exact ⟨S, ⟨equivToOpposite.symm.trans e⟩⟩
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := (a : α) → Option α) (fun (a : α) ↦ some a) some

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
y : β
o : Option α
⊢ y ∈ Option.map f o ↔ ∃ (x : α), x ∈ o ∧ f x = y

Tactic:
simp
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
H : Function.Injective f
a : α
o : Option α
⊢ f a ∈ Option.map f o ↔ a ∈ o

Tactic:
aesop
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
o : Option α
p : β → Prop
⊢ (∀ (y : β), y ∈ Option.map f o → p y) ↔ ∀ (x : α), x ∈ o → p (f x)

Tactic:
simp
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
o : Option α
p : β → Prop
⊢ (∃ (y : β), y ∈ Option.map f o ∧ p y) ↔ ∃ (x : α), x ∈ o ∧ p (f x)

Tactic:
simp
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
o : Option α
h : o.isSome = true
⊢ some (o.get h) = o

Tactic:
Option.some_get h

Premises used: Option.some_get
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
a : α
o1 o2 : Option α
h1 : a ∈ o1
h2 : a ∈ o2
⊢ o1 = o2

Tactic:
h1.trans h2.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
⊢ Relator.LeftUnique fun (x1 : α) (x2 : Option α) ↦ x1 ∈ x2

Tactic:
fun _ _ _ => mem_unique

Premises used: Option.mem_unique, Relator.LeftUnique
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_5
⊢ Function.Injective.{u_5 + 1, u_5 + 1} (α := α) some

Tactic:
fun _ _ ↦ some_inj.mp

Premises used: Iff.mp, Function.Injective, Option.some_inj
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Option.map f ∘ some = some ∘ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → Option β
x y : Option α
hx : x = y
hf : ∀ (a : α), a ∈ y → f a = g a
⊢ x.bind f = y.bind g

Tactic:
hx.symm ▸ bind_congr hf

Premises used: Eq.rec, Eq.symm, Option.bind_congr
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := (a : Option (Option α)) → Option α) joinM join

Tactic:
funext fun _ ↦ rfl

Premises used: funext, rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α β : Type u
f : α → Option β
x : Option α
⊢ x >>= f = x.bind f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α β : Type u_5
a : α
f : α → β
⊢ f <$> some a = some (f a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
⊢ Option.map f (some a) = some (f a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
h : Option.map f = Option.map g
x : α
⊢ some (f x) = some (g x)

Tactic:
simp only [← map_some, h]

Premises used: Option.map_some
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
⊢ Option.map f = Option.map g ↔ f = g

Tactic:
map_injective'.eq_iff

Premises used: Option.map_injective', Function.Injective.eq_iff
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
f : α → α
⊢ Option.map f = id ↔ f = id

Tactic:
map_injective'.eq_iff' map_id

Premises used: Option.map_injective', Function.Injective.eq_iff', Option.map_id
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
f₂ : α → γ
g₁ : β → δ
g₂ : γ → δ
h : g₁ ∘ f₁ = g₂ ∘ f₂
a : α
rw : Option.map (g₁ ∘ f₁) (some a) = Option.map g₂ (Option.map f₂ (some a))
rw₁ : Option.map (g₂ ∘ f₂) (some a) = Option.map g₂ (Option.map f₂ (some a))
rw₂ rw₃ : Option.map g₂ (Option.map f₂ (some a)) = Option.map g₂ (Option.map f₂ (some a))
⊢ Option.map g₁ (Option.map f₁ (some a)) = Option.map g₂ (Option.map f₂ (some a))

Tactic:
rw [map_map, h, ← map_map]

Premises used: Option.map_map
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha : a ∈ x
⊢ x = some a

Tactic:
rw [mem_def] at ha ⊢

Premises used: Option.mem_def
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha_1 : a ∈ x
ha : x = some a
subst : ∀ (h : ∀ (a_1 : α), a_1 ∈ some a → p a_1) (ha : a ∈ some a), pmap (p := p) f (some a) h = some (f a ⋯)
⊢ pmap (p := p) f x h = some (f a ⋯)

Tactic:
subst ha
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
ha : a ∈ some a
⊢ pmap (p := p) f (some a) h = some (f a ⋯)

Tactic:
rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α β γ : Type u_5
x : Option α
g : α → Option β
p : β → Prop
f : (b : β) → p b → γ
H : ∀ (a : β), x >>= g = some a → p a
H' : ∀ (a : α) (b : β), b ∈ g a → b ∈ x >>= g
⊢ pmap (p := p) f (x >>= g) H = do
    let a ← x
    pmap (p := p) f (g a) ⋯

Tactic:
grind [cases Option]

Premises used: Option
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_5
β γ : Type u_6
p : α → Prop
f : (a : α) → p a → β
x : Option α
g : β → Option γ
H : ∀ (a : α), x = some a → p a
⊢ pmap (p := p) f x H >>= g = x.pbind fun (a : α) (h : x = some a) ↦ g (f a ⋯)

Tactic:
grind [cases Option, pmap]

Premises used: Option.pmap, Option
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
x : Option α
f : (a : α) → a ∈ x → Option β
h' : ∀ (a : α) (H : a ∈ x), f a H = none → x = none
⊢ x.pbind f = none ↔ x = none

Tactic:
grind [cases Option]

Premises used: Option
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option (Option α)
H : ∀ (a : Option α), x = some a → ∀ (a_2 : α), a = some a_2 → p a_2
⊢ (pmap (p := fun (a : Option α) ↦ ∀ (a_1 : α), a = some a_1 → p a_1) (pmap (p := p) f) x H).join =
    pmap (p := p) f x.join ⋯

Tactic:
grind [cases Option]

Premises used: Option
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option (Option α)
H : ∀ (a : Option α), x = some a → ∀ (a_2 : α), a = some a_2 → p a_2
⊢ ((pmap (p := fun (a : Option α) ↦ ∀ (a_1 : α), a = some a_1 → p a_1) (pmap (p := p) f) x H).bind fun (a : Option β) ↦
      a) =
    pmap (p := p) f x.join ⋯

Tactic:
grind [cases Option]

Premises used: Option
-- Module: Mathlib.Data.Option.Basic
Goal:
α β : Type u_5
a : α
f : α → β
⊢ some f <*> some a = some (f a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
inst : Inhabited α
o : Option α
none : Eq.{u_1 + 1} (α := α) (getD Option.none default) (iget Option.none)
some : ∀ (val : α), (Option.some val).getD default = (Option.some val).iget
⊢ o.getD default = o.iget

Tactic:
cases o
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
inst : Inhabited α
⊢ Eq.{u_1 + 1} (α := α) (getD none default) (iget none)

Tactic:
rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
inst : Inhabited α
val : α
⊢ (some val).getD default = (some val).iget

Tactic:
rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_5
⊢ Eq.{u_5 + 1} (α := Option α) failure none

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
p : Prop
inst : Decidable p
u : Unit
⊢ _root_.guard p = some u ↔ p

Tactic:
grind [cases Option, _root_.guard]

Premises used: guard, Option
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
x : β
f : α → β
⊢ casesOn' none x f = x

Tactic:
rfl

Premises used: Option.casesOn', rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
x : β
f : α → β
a : α
⊢ (some a).casesOn' x f = f a

Tactic:
rfl

Premises used: Option.casesOn', rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
o : Option α
none : casesOn' (α := α) Option.none (f Option.none) (f ∘ fun (a : α) ↦ Option.some a) = f Option.none
some : ∀ (val : α), (Option.some val).casesOn' (f Option.none) (f ∘ fun (a : α) ↦ Option.some a) = f (Option.some val)
⊢ o.casesOn' (f Option.none) (f ∘ fun (a : α) ↦ Option.some a) = f o

Tactic:
cases o
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
⊢ casesOn' (α := α) none (f none) (f ∘ fun (a : α) ↦ some a) = f none

Tactic:
rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
val : α
⊢ (some val).casesOn' (f none) (f ∘ fun (a : α) ↦ some a) = f (some val)

Tactic:
rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
b : β
f : α → β
a : Option α
none : casesOn' Option.none b f = Option.elim Option.none b f
some : ∀ (val : α), (Option.some val).casesOn' b f = (Option.some val).elim b f
⊢ a.casesOn' b f = a.elim b f

Tactic:
cases a
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
b : β
f : α → β
⊢ casesOn' none b f = Option.elim none b f

Tactic:
rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
b : β
f : α → β
val : α
⊢ (some val).casesOn' b f = (some val).elim b f

Tactic:
rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
o o' : Option α
x : α
⊢ (o <|> o') = some x ↔ o = some x ∨ o = none ∧ o' = some x

Tactic:
simp
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
o o' : Option α
⊢ (o <|> o') = none ↔ o = none ∧ o' = none

Tactic:
simp
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_5
inst : IsEmpty α
⊢ choice α = none

Tactic:
choice_eq_none_iff_not_nonempty.mpr (not_nonempty_iff_imp_false.mpr isEmptyElim)

Premises used: Iff.mpr, isEmptyElim, not_nonempty_iff_imp_false, Option.choice_eq_none_iff_not_nonempty
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
i : Option α
none : Option.elim Option.none (f Option.none) (f ∘ Option.some) = f Option.none
some : ∀ (val : α), (Option.some val).elim (f Option.none) (f ∘ Option.some) = f (Option.some val)
⊢ i.elim (f Option.none) (f ∘ Option.some) = f i

Tactic:
cases i
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
⊢ Option.elim none (f none) (f ∘ some) = f none

Tactic:
rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
val : α
⊢ (some val).elim (f none) (f ∘ some) = f (some val)

Tactic:
rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
i : Option γ
none : (Option.elim Option.none (h x) fun (j : γ) ↦ h (f j)) = h (Option.elim Option.none x f)
some : ∀ (val : γ), ((Option.some val).elim (h x) fun (j : γ) ↦ h (f j)) = h ((Option.some val).elim x f)
⊢ (i.elim (h x) fun (j : γ) ↦ h (f j)) = h (i.elim x f)

Tactic:
cases i
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
⊢ (Option.elim none (h x) fun (j : γ) ↦ h (f j)) = h (Option.elim none x f)

Tactic:
rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
val : γ
⊢ ((some val).elim (h x) fun (j : γ) ↦ h (f j)) = h ((some val).elim x f)

Tactic:
rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
i : Option γ
none :
  (Option.elim Option.none (h x y) fun (j : γ) ↦ h (f j) (g j)) =
    h (Option.elim Option.none x f) (Option.elim Option.none y g)
some :
  ∀ (val : γ),
    ((Option.some val).elim (h x y) fun (j : γ) ↦ h (f j) (g j)) =
      h ((Option.some val).elim x f) ((Option.some val).elim y g)
⊢ (i.elim (h x y) fun (j : γ) ↦ h (f j) (g j)) = h (i.elim x f) (i.elim y g)

Tactic:
cases i
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
⊢ (Option.elim none (h x y) fun (j : γ) ↦ h (f j) (g j)) = h (Option.elim none x f) (Option.elim none y g)

Tactic:
rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
val : γ
⊢ ((some val).elim (h x y) fun (j : γ) ↦ h (f j) (g j)) = h ((some val).elim x f) ((some val).elim y g)

Tactic:
rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : γ → α → β
x : α → β
i : Option γ
y : α
rw rw₁ : i.elim x f y = i.elim x f y
⊢ i.elim x f y = i.elim (x y) fun (j : γ) ↦ f j y

Tactic:
rw [elim_comp fun f : α → β => f y]

Premises used: Option.elim_comp
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_5
β : Type u_6
inst : DecidableEq α
f : β
g : α → β
a : α
x : β
⊢ Option.elim' f (update (β := fun (a : α) ↦ β) g a x) =
    update (β := fun (a : Option α) ↦ β) (Option.elim' f g) (some a) x

Tactic:
Function.rec_update (α := fun _ => β) (@Option.some.inj _) (Option.elim' f) (fun _ _ => rfl) (fun
    | _, _, some _, h => (h _ rfl).elim
    | _, _, none, _ => rfl) _ _ _

Premises used: Option.elim', Option.some.inj, Function.rec_update, rfl
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
d : α
h : ∀ (x : α), ((fun (x : Option α) ↦ x.getD d) ∘ some) x = id x
⊢ Eq.{u_1 + 1} (α := α → α) ((fun (x : Option α) ↦ x.getD d) ∘ some) id

Tactic:
ext
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
d x : α
⊢ ((fun (x : Option α) ↦ x.getD d) ∘ some) x = id x

Tactic:
simp only [Function.comp_apply, getD_some, id_eq]

Premises used: Option.getD_some, Function.comp_apply, id_eq
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
x : Option α
f : α → β
rw : Option.map f x = none ↔ x = none
rw₁ rw₂ : x = none ↔ x = none
⊢ none = Option.map f x ↔ x = none

Tactic:
rw [eq_comm, map_eq_none_iff]

Premises used: eq_comm, Option.map_eq_none_iff
-- Module: Mathlib.Data.Option.Basic
Goal:
α : Type u_1
β : Type u_2
b : β
x : Option α
f : α → β
rw : Option.map f x = some b ↔ ∃ (a : α), x = some a ∧ f a = b
rw₁ rw₂ : (∃ (a : α), x = some a ∧ f a = b) ↔ ∃ (a : α), x = some a ∧ f a = b
⊢ some b = Option.map f x ↔ ∃ (a : α), x = some a ∧ f a = b

Tactic:
rw [eq_comm, map_eq_some_iff]

Premises used: eq_comm, Option.map_eq_some_iff
-- Module: Mathlib.Data.Option.Defs
Goal:
α : Type u_1
β : Type u_2
b : β
f : α → β
⊢ Option.elim' b f none = b

Tactic:
rfl

Premises used: Option.elim', rfl
-- Module: Mathlib.Data.Option.Defs
Goal:
α : Type u_1
β : Type u_2
a : α
b : β
f : α → β
⊢ Option.elim' b f (some a) = f a

Tactic:
rfl

Premises used: Option.elim', rfl
-- Module: Mathlib.Data.Option.Defs
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
o : Option α
none : Option.elim' (f Option.none) (f ∘ Option.some) Option.none = f Option.none
some : ∀ (val : α), Option.elim' (f Option.none) (f ∘ Option.some) (Option.some val) = f (Option.some val)
⊢ Option.elim' (f Option.none) (f ∘ Option.some) o = f o

Tactic:
cases o
-- Module: Mathlib.Data.Option.Defs
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
⊢ Option.elim' (f none) (f ∘ some) none = f none

Tactic:
rfl
-- Module: Mathlib.Data.Option.Defs
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
val : α
⊢ Option.elim' (f none) (f ∘ some) (some val) = f (some val)

Tactic:
rfl
-- Module: Mathlib.Data.Option.Defs
Goal:
α : Type u_3
β : Type u_4
b : β
f : α → β
a : Option α
none : Option.elim' b f Option.none = Option.elim Option.none b f
some : ∀ (val : α), Option.elim' b f (Option.some val) = (Option.some val).elim b f
⊢ Option.elim' b f a = a.elim b f

Tactic:
cases a
-- Module: Mathlib.Data.Option.Defs
Goal:
α : Type u_3
β : Type u_4
b : β
f : α → β
⊢ Option.elim' b f none = Option.elim none b f

Tactic:
rfl
-- Module: Mathlib.Data.Option.Defs
Goal:
α : Type u_3
β : Type u_4
b : β
f : α → β
val : α
⊢ Option.elim' b f (some val) = (some val).elim b f

Tactic:
rfl
-- Module: Mathlib.Data.Option.Defs
Goal:
α : Type u_1
inst : Inhabited α
a : α
⊢ (some a).iget = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Option.NAry
Goal:
α β γ : Type u
f : α → β → γ
a : Option α
b : Option β
none : map₂ f Option.none b = f <$> Option.none <*> b
some : ∀ (val : α), map₂ f (Option.some val) b = f <$> Option.some val <*> b
⊢ map₂ f a b = f <$> a <*> b

Tactic:
cases a
-- Module: Mathlib.Data.Option.NAry
Goal:
α β γ : Type u
f : α → β → γ
b : Option β
⊢ map₂ f none b = f <$> none <*> b

Tactic:
rfl
-- Module: Mathlib.Data.Option.NAry
Goal:
α β γ : Type u
f : α → β → γ
b : Option β
val : α
⊢ map₂ f (some val) b = f <$> some val <*> b

Tactic:
rfl
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
b : β
⊢ map₂ f (some a) (some b) = some (f a b)

Tactic:
rfl

Premises used: rfl, Option.map₂
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : Option β
⊢ map₂ f none b = none

Tactic:
rfl

Premises used: rfl, Option.map₂
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
none : map₂ f Option.none Option.none = Option.none
some : ∀ (val : α), map₂ f (Option.some val) Option.none = Option.none
⊢ map₂ f a Option.none = Option.none

Tactic:
cases a
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
⊢ map₂ f none none = none

Tactic:
rfl
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
val : α
⊢ map₂ f (some val) none = none

Tactic:
rfl
-- Module: Mathlib.Data.Option.NAry
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
b : Option β
⊢ map₂ f (some a) b = Option.map (fun (b : β) ↦ f a b) b

Tactic:
rfl

Premises used: rfl, Option.map₂