awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Functor
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
E1 : ∀ {α β : Type u_1}, Eq (α := α → F β → F α) mapConst (map ∘ Function.const β)
E2 : ∀ {α β : Type u_1}, Eq (α := α → F β → F α) mapConst (map ∘ Function.const β)
⊢ Eq (α := α → F β → F α) mc mc'

Tactic:
E1.trans E2.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Control.Functor
Goal:
F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
E1 : ∀ {α β : Type u_1}, Eq (α := α → F β → F α) mapConst (map ∘ Function.const β)
E2 : ∀ {α β : Type u_1}, Eq (α := α → F β → F α) mapConst (map ∘ Function.const β)
⊢ Eq (α := α → F β → F α) mc mc'

Tactic:
exact E1.trans E2.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Control.Functor
Goal:
α : Type u_1
β : Type u_2
x y : Const α β
h : x.run = y.run
⊢ x = y

Tactic:
h

Premises used: Functor.Const.run, Functor.Const
-- Module: Mathlib.Control.Functor
Goal:
γ : Type u_1
map_const : ∀ {α β : Type u_2}, Eq (α := α → Const γ β → Const γ α) mapConst (map ∘ Function.const β)
id_map : ∀ {α : Type u_2} (x : Const γ α), id <$> x = x
comp_map : ∀ {α β γ_1 : Type u_2} (g : α → β) (h : β → γ_1) (x : Const γ α), (h ∘ g) <$> x = h <$> g <$> x
⊢ LawfulFunctor.{u_2, u_1} (Const γ)

Tactic:
constructor
-- Module: Mathlib.Control.Functor
Goal:
γ : Type u_1
α β : Type u_2
⊢ Eq (α := α → Const γ β → Const γ α) mapConst (map ∘ Function.const β)

Tactic:
rfl
-- Module: Mathlib.Control.Functor
Goal:
γ : Type u_1
α : Type u_2
x : Const γ α
⊢ id <$> x = x

Tactic:
rfl
-- Module: Mathlib.Control.Functor
Goal:
γ : Type u_1
α β γ_1 : Type u_2
g : α → β
h : β → γ_1
x : Const γ α
⊢ (h ∘ g) <$> x = h <$> g <$> x

Tactic:
rfl
-- Module: Mathlib.Control.Functor
Goal:
γ : Type u_1
⊢ LawfulFunctor.{u_2, u_1} (AddConst γ)

Tactic:
@Const.lawfulFunctor γ

Premises used: Functor.Const.lawfulFunctor, Functor.AddConst
-- Module: Mathlib.Control.Functor
Goal:
F : Type u → Type w
G : Type v → Type u
α : Type v
x y : Comp F G α
⊢ x.run = y.run → x = y

Tactic:
id

Premises used: id, Functor.Comp.run, Functor.Comp
-- Module: Mathlib.Control.Functor
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Functor F
inst_1 : Functor G
α β : Type v
h : α → β
x : F (G α)
⊢ h <$> mk x = mk ((fun (x : G α) ↦ h <$> x) <$> x)

Tactic:
rfl

Premises used: Functor.Comp.map, Functor.Comp.mk, rfl
-- Module: Mathlib.Control.Functor
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Functor F
inst_1 : Functor G
α β : Type v
h : α → β
x : Comp F G α
⊢ (h <$> x).run = (fun (x : G α) ↦ h <$> x) <$> x.run

Tactic:
rfl

Premises used: Functor.Comp.map, Functor.Comp.mk, Functor.Comp.run, rfl
-- Module: Mathlib.Control.Functor
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Functor F
inst_1 : Functor G
inst_2 : LawfulFunctor F
inst_3 : LawfulFunctor G
α : Type v
x : F (G α)
simp : mk (mk x) = mk x
⊢ Comp.map id (mk x) = mk x

Tactic:
simp only [Comp.map, id_map, id_map']

Premises used: Functor.Comp.map, id_map', LawfulFunctor.id_map
-- Module: Mathlib.Control.Functor
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Functor F
inst_1 : Functor G
inst_2 : LawfulFunctor F
inst_3 : LawfulFunctor G
α : Type v
x : F (G α)
⊢ mk (mk x) = mk x

Tactic:
rfl
-- Module: Mathlib.Control.Functor
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Functor F
inst_1 : Functor G
inst_2 : LawfulFunctor F
inst_3 : LawfulFunctor G
α β γ : Type v
g' : α → β
h : β → γ
x : F (G α)
⊢ Comp.map (h ∘ g') (mk x) = Comp.map h (Comp.map g' (mk x))

Tactic:
simp [Comp.map, Comp.mk, functor_norm, Function.comp_def]

Premises used: Functor.Comp.map, Function.comp_def, Functor.Comp.mk
-- Module: Mathlib.Control.Functor
Goal:
F : Type u_1 → Type u_2
AF : Functor F
inst : LawfulFunctor F
⊢ functor = AF

Tactic:
@Functor.ext F _ AF (Comp.lawfulFunctor (G := Id)) _ fun _ _ _ _ => rfl

Premises used: Functor.ext, Id, Functor.Comp, rfl
-- Module: Mathlib.Control.Functor
Goal:
F : Type u_1 → Type u_2
AF : Functor F
inst : LawfulFunctor F
⊢ functor = AF

Tactic:
@Functor.ext F _ AF (Comp.lawfulFunctor (F := Id)) _ fun _ _ _ _ => rfl

Premises used: Functor.ext, Id, Functor.Comp, rfl
-- Module: Mathlib.Control.Functor
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
α β : Type v
f : Comp F G (α → β)
x : Comp F G α
⊢ (f <*> x).run = (fun (x1 : G (α → β)) (x2 : G α) ↦ x1 <*> x2) <$> f.run <*> x.run

Tactic:
rfl

Premises used: Functor.Comp.seq, Functor.Comp.mk, Functor.Comp.run, rfl
-- Module: Mathlib.Control.Functor
Goal:
F : Type u → Type v
inst : Functor F
α : Type u
x : F α
p : α → Prop
h : Liftp p x
⊢ ∀ (y : α), y ∈ supp x → p y

Tactic:
fun _ hy => hy h
-- Module: Mathlib.Control.Lawful
Goal:
σ : Type u
m : Type u → Type v
α β : Type u
inst : Monad m
⊢ Eq (α := α → StateT σ m β → StateT σ m α) Functor.mapConst (Functor.map ∘ Function.const β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Lawful
Goal:
σ : Type u
m : Type u → Type v
α β : Type u
inst : Monad m
inst_1 : LawfulMonad m
x : StateT σ m α
y : β
st : σ
⊢ (Functor.mapConst y x).run st = Prod.map (Function.const α y) id <$> x.run st

Tactic:
run_map _ _ _

Premises used: Prod.map, StateT.run_map
-- Module: Mathlib.Control.Lawful
Goal:
α ε : Type u
m : Type u → Type v
n : Type u → Type u_1
inst : Monad m
inst_1 : MonadLiftT n m
x : n α
⊢ Eq.{v + 1} (α := m (Except ε α)) (run (monadLift x)) (Except.ok <$> monadLift x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
zero :
  LE.le (α := (a : α) → Part (β a)) (⊥ : (a : α) → Part (β a))
    ((f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) ⊥ : (a : α) → Part (β a))
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (Nat.succ 0))

Tactic:
dsimp [approx]

Premises used: Part.Fix.approx
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ LE.le (α := (a : α) → Part (β a)) (⊥ : (a : α) → Part (β a))
    ((f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) ⊥ : (a : α) → Part (β a))

Tactic:
apply @bot_le _ _ _ (f ⊥)

Premises used: bot_le
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n : ℕ
i_ih :
  LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n.succ)
i : α
succ :
  LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (n + 1))
⊢ LE.le.{u_2} (α := (fun (a : α) ↦ Part.{u_2} (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (n + 1) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (n + 1).succ i)

Tactic:
apply f.monotone

Premises used: OrderHom.monotone
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n : ℕ
i_ih :
  LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n.succ)
i : α
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (n + 1))

Tactic:
apply i_ih
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
zero :
  LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (Nat.succ 0))
succ :
  ∀ (n : ℕ)
    (i_ih :
      LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n)
        (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n.succ)),
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (n + 1))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (n + 1).succ)
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i.succ)

Tactic:
induction i with
  | zero => dsimp [approx]; apply @bot_le _ _ _ (f ⊥)
  | succ _ i_ih => intro; apply f.monotone; apply i_ih

Premises used: OrderHom.monotone, Part.Fix.approx, bot_le
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
hij : i ≤ 0
zero :
  LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)

Tactic:
cases hij
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih :
  ∀ (hij : i ≤ j),
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j)
hij : i ≤ j + 1
succ :
  ∀
    (ih :
      ∀ (hij : j + 1 ≤ j),
        LE.le (α := (a : α) → Part (β a))
          (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
          (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j)),
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
succ₁ :
  i.le j →
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))

Tactic:
cases hij
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j : ℕ
ih :
  ∀ (hij : j + 1 ≤ j),
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j)
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j : ℕ
ih :
  ∀ (hij : j + 1 ≤ j),
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j)
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih :
  ∀ (hij : i ≤ j),
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j)
h : i.le j
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))

Tactic:
le_trans (ih ‹_›) (approx_mono' f)

Premises used: Part.Fix.approx_mono', le_trans
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih :
  ∀ (hij : i ≤ j),
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j)
h : i.le j
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))

Tactic:
exact le_trans (ih ‹_›) (approx_mono' f)

Premises used: Part.Fix.approx_mono', le_trans
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij : i ≤ j
zero :
  ∀ (hij : i ≤ 0),
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) 0)
succ :
  ∀ (j : ℕ)
    (ih :
      ∀ (hij : i ≤ j),
        LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
          (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j))
    (hij : i ≤ j + 1),
    LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) (j + 1))
⊢ LE.le (α := (a : α) → Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) j)

Tactic:
induction j with
  | zero => cases hij; exact le_rfl
  | succ j ih =>
    cases hij; · exact le_rfl
    exact le_trans (ih ‹_›) (approx_mono' f)

Premises used: le_rfl
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
pos :
  ∀
    (h₀ :
      ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)),
    Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
      ∃ (i : ℕ),
        Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
          b
neg :
  ∀
    (h₀ :
      ¬∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)),
    Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
      ∃ (i : ℕ),
        Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
          b
⊢ Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b

Tactic:
by_cases h₀ : ∃ i : ℕ, (approx f i a).Dom
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
pos :
  Membership.mem (γ := Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        (Nat.find (p := fun (n : ℕ) ↦
            Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a))
            h₀).succ
        a)
      b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
⊢ Membership.mem (γ := Part (β a)) (Part.fix (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) a) b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b

Tactic:
simp only [Part.fix_def f h₀]

Premises used: Part.fix_def, DFunLike.coe
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
pos :
  Membership.mem (γ := Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        (Nat.find (p := fun (n : ℕ) ↦
            Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a))
            h₀).succ
        a)
      b →
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
pos₁ :
  (∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
        b) →
    Membership.mem (γ := Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        (Nat.find (p := fun (n : ℕ) ↦
            Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a))
            h₀).succ
        a)
      b
⊢ Membership.mem (γ := Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        (Nat.find (p := fun (n : ℕ) ↦
            Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a))
            h₀).succ
        a)
      b ↔
    ∃ (i : ℕ),
      Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b

Tactic:
constructor
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
hh :
  Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    b
⊢ ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b

Tactic:
⟨_, hh⟩

Premises used: Exists.intro
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
hh :
  Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    b
⊢ ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b

Tactic:
exact ⟨_, hh⟩
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
hh :
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
⊢ Dom.{u_2} (α := β a)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
        Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀)
      a)

Tactic:
have h₁ := Nat.find_spec h₀
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
hh :
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
h₁ :
  Dom.{u_2} (α := β a)
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
        Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀)
      a)
⊢ ∃ (y : β a),
    Membership.mem (γ := Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀)
        a)
      y

Tactic:
rw [dom_iff_mem] at h₁

Premises used: Part.dom_iff_mem
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ (i : ℕ), Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a)
hh :
  ∃ (i : ℕ),
    Membership.mem (γ := Part (β a)) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) i a) b
h₁ :
  ∃ (y : β a),
    Membership.mem (γ := Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀)
        a)
      y
pos :
  ∀ (y : β a)
    (h₁ :
      Membership.mem (γ := Part (β a))
        (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
          (Nat.find (p := fun (n : ℕ) ↦
            Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀)
          a)
        y),
    Membership.mem (γ := Part (β a))
      (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
        (Nat.find (p := fun (n : ℕ) ↦
            Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a))
            h₀).succ
        a)
      b
⊢ Membership.mem (γ := Part (β a))
    (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a))
      (Nat.find (p := fun (n : ℕ) ↦
          Dom.{u_2} (α := β a) (approx (β := β) (⇑f : (a : (a : α) → Part (β a)) → (a : α) → Part (β a)) n a)) h₀).succ
      a)
    b

Tactic:
obtain ⟨y, h₁⟩ := h₁