[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable α
x y : α
e : encode x = encode y
⊢ some x = some y
[PROOFSTEP]
rw [← encodek, e, encodek]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Inhabited α
x : α
⊢ (fun n => iget (decode n)) (encode x) = x
[PROOFSTEP]
simp_rw [Encodable.encodek]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable α
f : β → α
finv : α → Option β
linv : ∀ (b : β), finv (f b) = some b
b : β
⊢ (fun n => Option.bind (decode n) finv) ((fun b => encode (f b)) b) = some b
[PROOFSTEP]
simp [Encodable.encodek, linv]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
inst✝ : Encodable α
e : β ≃ α
n : ℕ
⊢ Option.bind (decode n) (some ∘ ↑e.symm) = Option.map (↑e.symm) (decode n)
[PROOFSTEP]
rw [Option.map_eq_bind]
[GOAL]
α : Type u_1
β : Type u_2
x✝ : PUnit
⊢ (fun n => Nat.casesOn n (some PUnit.unit) fun x => none) ((fun x => 0) x✝) = some x✝
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
o : Option α
⊢ (fun n => Nat.casesOn n (some none) fun m => Option.map some (decode m))
      ((fun o => Option.casesOn o zero fun a => succ (encode a)) o) =
    some o
[PROOFSTEP]
cases o
[GOAL]
case none
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
⊢ (fun n => Nat.casesOn n (some none) fun m => Option.map some (decode m))
      ((fun o => Option.casesOn o zero fun a => succ (encode a)) none) =
    some none
[PROOFSTEP]
dsimp
[GOAL]
case some
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
val✝ : α
⊢ (fun n => Nat.casesOn n (some none) fun m => Option.map some (decode m))
      ((fun o => Option.casesOn o zero fun a => succ (encode a)) (some val✝)) =
    some (some val✝)
[PROOFSTEP]
dsimp
[GOAL]
case some
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
val✝ : α
⊢ Option.map some (decode (encode val✝)) = some (some val✝)
[PROOFSTEP]
simp [encodek, Nat.succ_ne_zero]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable α
n : ℕ
a : α
⊢ a ∈ decode₂ α n ↔ a ∈ decode n ∧ encode a = n
[PROOFSTEP]
simp [decode₂]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable α
n : ℕ
a : α
⊢ (∃ a_1, decode n = some a_1 ∧ a_1 = a ∧ encode a_1 = n) ↔ decode n = some a ∧ encode a = n
[PROOFSTEP]
exact ⟨fun ⟨_, h₁, rfl, h₂⟩ => ⟨h₁, h₂⟩, fun ⟨h₁, h₂⟩ => ⟨_, h₁, rfl, h₂⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable α
a : α
⊢ decode₂ α (encode a) = some a
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : Encodable α
a a✝ : α
⊢ a✝ ∈ decode₂ α (encode a) ↔ a✝ ∈ some a
[PROOFSTEP]
simp [mem_decode₂, eq_comm, decode₂_eq_some]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Encodable α
n : ℕ
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range encode
[PROOFSTEP]
simp_rw [Set.range, Set.mem_setOf_eq, Ne.def, Option.eq_none_iff_forall_not_mem, Encodable.mem_decode₂, not_forall,
  not_not]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
h : isSome (decode₂ α x) = true
⊢ encode (Option.get (decode₂ α x) h) = x
[PROOFSTEP]
rw [← decode₂_is_partial_inv (Option.get _ h), Option.some_get]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
x✝ : (fun x => x ∈ Set.range encode) x
n : α
hn : encode n = x
⊢ isSome (decode₂ α x) = true
[PROOFSTEP]
rw [← hn, encodek₂]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
x✝ : (fun x => x ∈ Set.range encode) x
n : α
hn : encode n = x
⊢ isSome (some n) = true
[PROOFSTEP]
exact rfl
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
⊢ isSome (decode₂ α ↑n) = true
[PROOFSTEP]
cases' n.2 with x hx
[GOAL]
case intro
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
x : α
hx : encode x = ↑n
⊢ isSome (decode₂ α ↑n) = true
[PROOFSTEP]
rw [← hx, encodek₂]
[GOAL]
case intro
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
n : ↑(Set.range encode)
x : α
hx : encode x = ↑n
⊢ isSome (some x) = true
[PROOFSTEP]
exact rfl
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
a : α
⊢ (fun n => Option.get (decode₂ α ↑n) (_ : isSome (decode₂ α ↑n) = true))
      ((fun a => { val := encode a, property := (_ : encode a ∈ Set.range encode) }) a) =
    a
[PROOFSTEP]
dsimp
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
a : α
⊢ Option.get (decode₂ α (encode a)) (_ : isSome (decode₂ α (encode a)) = true) = a
[PROOFSTEP]
rw [← Option.some_inj, Option.some_get, encodek₂]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : ↑(Set.range encode)
n : ℕ
x : α
hx : encode x = n
⊢ (fun a => { val := encode a, property := (_ : encode a ∈ Set.range encode) })
      ((fun n => Option.get (decode₂ α ↑n) (_ : isSome (decode₂ α ↑n) = true))
        { val := n, property := (_ : ∃ y, encode y = n) }) =
    { val := n, property := (_ : ∃ y, encode y = n) }
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case a
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : ↑(Set.range encode)
n : ℕ
x : α
hx : encode x = n
⊢ ↑((fun a => { val := encode a, property := (_ : encode a ∈ Set.range encode) })
        ((fun n => Option.get (decode₂ α ↑n) (_ : isSome (decode₂ α ↑n) = true))
          { val := n, property := (_ : ∃ y, encode y = n) })) =
    ↑{ val := n, property := (_ : ∃ y, encode y = n) }
[PROOFSTEP]
dsimp
[GOAL]
case a
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : ↑(Set.range encode)
n : ℕ
x : α
hx : encode x = n
⊢ encode (Option.get (decode₂ α n) (_ : isSome (decode₂ α n) = true)) = n
[PROOFSTEP]
conv =>
  rhs
  rw [← hx]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : ↑(Set.range encode)
n : ℕ
x : α
hx : encode x = n
| encode (Option.get (decode₂ α n) (_ : isSome (decode₂ α n) = true)) = n
[PROOFSTEP]
  rhs
  rw [← hx]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : ↑(Set.range encode)
n : ℕ
x : α
hx : encode x = n
| encode (Option.get (decode₂ α n) (_ : isSome (decode₂ α n) = true)) = n
[PROOFSTEP]
  rhs
  rw [← hx]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : ↑(Set.range encode)
n : ℕ
x : α
hx : encode x = n
| encode (Option.get (decode₂ α n) (_ : isSome (decode₂ α n) = true)) = n
[PROOFSTEP]
rhs
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : ↑(Set.range encode)
n : ℕ
x : α
hx : encode x = n
| n
[PROOFSTEP]
rw [← hx]
[GOAL]
case a
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x✝ : ↑(Set.range encode)
n : ℕ
x : α
hx : encode x = n
⊢ encode (Option.get (decode₂ α n) (_ : isSome (decode₂ α n) = true)) = encode x
[PROOFSTEP]
rw [encode_injective.eq_iff, ← Option.some_inj, Option.some_get, ← hx, encodek₂]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
s : α ⊕ β
⊢ decodeSum (encodeSum s) = some s
[PROOFSTEP]
cases s
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
val✝ : α
⊢ decodeSum (encodeSum (Sum.inl val✝)) = some (Sum.inl val✝)
[PROOFSTEP]
simp [encodeSum, div2_val, decodeSum, encodek]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
val✝ : β
⊢ decodeSum (encodeSum (Sum.inr val✝)) = some (Sum.inr val✝)
[PROOFSTEP]
simp [encodeSum, div2_val, decodeSum, encodek]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
h : 2 ≤ n
⊢ decode n = none
[PROOFSTEP]
suffices decodeSum n = none by
  change (decodeSum n).bind _ = none
  rw [this]
  rfl
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ decode n = none
[PROOFSTEP]
change (decodeSum n).bind _ = none
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ Option.bind (decodeSum n) (some ∘ ↑Equiv.boolEquivPUnitSumPUnit.symm) = none
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ Option.bind none (some ∘ ↑Equiv.boolEquivPUnitSumPUnit.symm) = none
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
h : 2 ≤ n
⊢ decodeSum n = none
[PROOFSTEP]
have : 1 ≤ n / 2 := by
  rw [Nat.le_div_iff_mul_le]
  exacts [h, by decide]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
h : 2 ≤ n
⊢ 1 ≤ n / 2
[PROOFSTEP]
rw [Nat.le_div_iff_mul_le]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
h : 2 ≤ n
⊢ 1 * 2 ≤ n
α : Type u_1 β : Type u_2 n : ℕ h : 2 ≤ n ⊢ 0 < 2
[PROOFSTEP]
exacts [h, by decide]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
h : 2 ≤ n
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
⊢ decodeSum n = none
[PROOFSTEP]
cases' exists_eq_succ_of_ne_zero (_root_.ne_of_gt this) with m e
[GOAL]
case intro
α : Type u_1
β : Type u_2
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = succ m
⊢ decodeSum n = none
[PROOFSTEP]
simp [decodeSum, div2_val]
[GOAL]
case intro
α : Type u_1
β : Type u_2
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = succ m
⊢ (match (bodd n, n / 2) with
    | (false, m) => Option.map Sum.inl (decode m)
    | (fst, m) => Option.map Sum.inr (decode m)) =
    none
[PROOFSTEP]
cases bodd n
[GOAL]
case intro.false
α : Type u_1
β : Type u_2
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = succ m
⊢ (match (false, n / 2) with
    | (false, m) => Option.map Sum.inl (decode m)
    | (fst, m) => Option.map Sum.inr (decode m)) =
    none
[PROOFSTEP]
simp [e]
[GOAL]
case intro.true
α : Type u_1
β : Type u_2
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = succ m
⊢ (match (true, n / 2) with
    | (false, m) => Option.map Sum.inl (decode m)
    | (fst, m) => Option.map Sum.inr (decode m)) =
    none
[PROOFSTEP]
simp [e]
[GOAL]
α : Type u_1
β : Type u_2
γ : α → Type u_3
inst✝¹ : Encodable α
inst✝ : (a : α) → Encodable (γ a)
x✝ : Sigma γ
a : α
b : γ a
⊢ decodeSigma (encodeSigma { fst := a, snd := b }) = some { fst := a, snd := b }
[PROOFSTEP]
simp [encodeSigma, decodeSigma, unpair_pair, encodek]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
i : Encodable α
n : ℕ
⊢ decode n = Option.bind (decode (unpair n).fst) fun a => Option.map (Prod.mk a) (decode (unpair n).snd)
[PROOFSTEP]
simp only [decode_ofEquiv, Equiv.symm_symm, decode_sigma_val]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
i : Encodable α
n : ℕ
⊢ Option.map (↑(Equiv.sigmaEquivProd α β))
      (Option.bind (decode (unpair n).fst) fun a => Option.map (Sigma.mk a) (decode (unpair n).snd)) =
    Option.bind (decode (unpair n).fst) fun a => Option.map (Prod.mk a) (decode (unpair n).snd)
[PROOFSTEP]
cases (decode n.unpair.1 : Option α)
[GOAL]
case none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
i : Encodable α
n : ℕ
⊢ Option.map (↑(Equiv.sigmaEquivProd α β)) (Option.bind none fun a => Option.map (Sigma.mk a) (decode (unpair n).snd)) =
    Option.bind none fun a => Option.map (Prod.mk a) (decode (unpair n).snd)
[PROOFSTEP]
cases (decode n.unpair.2 : Option β)
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
i : Encodable α
n : ℕ
val✝ : α
⊢ Option.map (↑(Equiv.sigmaEquivProd α β))
      (Option.bind (some val✝) fun a => Option.map (Sigma.mk a) (decode (unpair n).snd)) =
    Option.bind (some val✝) fun a => Option.map (Prod.mk a) (decode (unpair n).snd)
[PROOFSTEP]
cases (decode n.unpair.2 : Option β)
[GOAL]
case none.none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
i : Encodable α
n : ℕ
⊢ Option.map (↑(Equiv.sigmaEquivProd α β)) (Option.bind none fun a => Option.map (Sigma.mk a) none) =
    Option.bind none fun a => Option.map (Prod.mk a) none
[PROOFSTEP]
rfl
[GOAL]
case none.some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
i : Encodable α
n : ℕ
val✝ : β
⊢ Option.map (↑(Equiv.sigmaEquivProd α β)) (Option.bind none fun a => Option.map (Sigma.mk a) (some val✝)) =
    Option.bind none fun a => Option.map (Prod.mk a) (some val✝)
[PROOFSTEP]
rfl
[GOAL]
case some.none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
i : Encodable α
n : ℕ
val✝ : α
⊢ Option.map (↑(Equiv.sigmaEquivProd α β)) (Option.bind (some val✝) fun a => Option.map (Sigma.mk a) none) =
    Option.bind (some val✝) fun a => Option.map (Prod.mk a) none
[PROOFSTEP]
rfl
[GOAL]
case some.some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
i : Encodable α
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map (↑(Equiv.sigmaEquivProd α β)) (Option.bind (some val✝¹) fun a => Option.map (Sigma.mk a) (some val✝)) =
    Option.bind (some val✝¹) fun a => Option.map (Prod.mk a) (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
P : α → Prop
encA : Encodable α
decP : DecidablePred P
x✝ : { a // P a }
v : α
h : P v
⊢ decodeSubtype (encodeSubtype { val := v, property := h }) = some { val := v, property := h }
[PROOFSTEP]
simp [encodeSubtype, decodeSubtype, encodek, h]
[GOAL]
α : Type u_1
β : Type u_2
P : α → Prop
encA : Encodable α
decP : DecidablePred P
a : Subtype P
⊢ encode a = encode ↑a
[PROOFSTEP]
cases a
[GOAL]
case mk
α : Type u_1
β : Type u_2
P : α → Prop
encA : Encodable α
decP : DecidablePred P
val✝ : α
property✝ : P val✝
⊢ encode { val := val✝, property := property✝ } = encode ↑{ val := val✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
⊢ Countable ℕ+
[PROOFSTEP]
delta PNat
[GOAL]
⊢ Countable { n // 0 < n }
[PROOFSTEP]
infer_instance
  -- short-circuit instance search
[GOAL]
α : Type u_1
inst✝ : Encodable α
⊢ DecidableEq (ULower α)
[PROOFSTEP]
delta ULower
[GOAL]
α : Type u_1
inst✝ : Encodable α
⊢ DecidableEq ↑(Set.range Encodable.encode)
[PROOFSTEP]
exact Encodable.decidableEqOfEncodable _
[GOAL]
α : Type u_1
inst✝ : Encodable α
⊢ Encodable (ULower α)
[PROOFSTEP]
delta ULower
[GOAL]
α : Type u_1
inst✝ : Encodable α
⊢ Encodable ↑(Set.range Encodable.encode)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝ : Encodable α
a : α
⊢ up (down a) = a
[PROOFSTEP]
simp [up, down, Equiv.left_inv _ _, Equiv.symm_apply_apply]
[GOAL]
α : Type u_1
p : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred p
n : Option α
⊢ Decidable (Encodable.good p n)
[PROOFSTEP]
cases n
[GOAL]
case none
α : Type u_1
p : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred p
⊢ Decidable (Encodable.good p none)
[PROOFSTEP]
unfold good
[GOAL]
case some
α : Type u_1
p : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred p
val✝ : α
⊢ Decidable (Encodable.good p (some val✝))
[PROOFSTEP]
unfold good
[GOAL]
case none
α : Type u_1
p : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred p
⊢ Decidable
    (match none with
    | some a => p a
    | none => False)
[PROOFSTEP]
dsimp
[GOAL]
case some
α : Type u_1
p : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred p
val✝ : α
⊢ Decidable
    (match some val✝ with
    | some a => p a
    | none => False)
[PROOFSTEP]
dsimp
[GOAL]
case none
α : Type u_1
p : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred p
⊢ Decidable False
[PROOFSTEP]
infer_instance
[GOAL]
case some
α : Type u_1
p : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred p
val✝ : α
⊢ Decidable (p val✝)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
p : α → Prop
inst✝¹ : Encodable α
inst✝ : DecidablePred p
h : ∃ x, p x
w : α
pw : p w
⊢ Encodable.good p (decode (encode w))
[PROOFSTEP]
simp [good, encodek, pw]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
⊢ r (f (Directed.sequence f hf n)) (f (Directed.sequence f hf (n + 1)))
[PROOFSTEP]
dsimp [Directed.sequence]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
⊢ r (f (Directed.sequence f hf n))
    (f
      (match decode n with
      | none =>
        Classical.choose (_ : ∃ z, r (f (Directed.sequence f hf n)) (f z) ∧ r (f (Directed.sequence f hf n)) (f z))
      | some a => Classical.choose (_ : ∃ z, r (f (Directed.sequence f hf n)) (f z) ∧ r (f a) (f z))))
[PROOFSTEP]
generalize hf.sequence f n = p
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
⊢ r (f p)
    (f
      (match decode n with
      | none => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f p) (f z))
      | some a => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f a) (f z))))
[PROOFSTEP]
cases' h : (decode n : Option α) with a
[GOAL]
case none
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
h : decode n = none
⊢ r (f p)
    (f
      (match none with
      | none => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f p) (f z))
      | some a => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f a) (f z))))
[PROOFSTEP]
exact (Classical.choose_spec (hf p p)).1
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p a : α
h : decode n = some a
⊢ r (f p)
    (f
      (match some a with
      | none => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f p) (f z))
      | some a => Classical.choose (_ : ∃ z, r (f p) (f z) ∧ r (f a) (f z))))
[PROOFSTEP]
exact (Classical.choose_spec (hf p a)).1
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a) (f (Directed.sequence f hf (encode a + 1)))
[PROOFSTEP]
simp only [Directed.sequence, add_eq, add_zero, encodek, and_self]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a) (f (Classical.choose (_ : ∃ x, (fun x => r (f (Directed.sequence f hf (encode a))) (f x) ∧ r (f a) (f x)) x)))
[PROOFSTEP]
exact (Classical.choose_spec (hf _ a)).2
[GOAL]
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x x_1 => x ≈ x_1
inst✝ : Encodable α
⊢ ∀ (a : Quotient s), (fun n => Quotient.mk'' <$> decode n) ((fun q => encode (rep q)) a) = some a
[PROOFSTEP]
rintro ⟨l⟩
[GOAL]
case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x x_1 => x ≈ x_1
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ (fun n => Quotient.mk'' <$> decode n) ((fun q => encode (rep q)) (Quot.mk Setoid.r l)) = some (Quot.mk Setoid.r l)
[PROOFSTEP]
dsimp
[GOAL]
case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x x_1 => x ≈ x_1
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ Option.map Quotient.mk'' (decode (encode (rep (Quot.mk Setoid.r l)))) = some (Quot.mk Setoid.r l)
[PROOFSTEP]
rw [encodek]
[GOAL]
case mk
α : Type u_1
s : Setoid α
inst✝¹ : DecidableRel fun x x_1 => x ≈ x_1
inst✝ : Encodable α
a✝ : Quotient s
l : α
⊢ Option.map Quotient.mk'' (some (rep (Quot.mk Setoid.r l))) = some (Quot.mk Setoid.r l)
[PROOFSTEP]
exact congr_arg some ⟦l⟧.rep_spec


[GOAL]
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
h : α ≃ β
x : f α
⊢ ↑h.symm <$> ↑h <$> x = x
[PROOFSTEP]
simp [map_map]
[GOAL]
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
h : α ≃ β
x : f β
⊢ ↑h <$> ↑h.symm <$> x = x
[PROOFSTEP]
simp [map_map]
[GOAL]
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
[PROOFSTEP]
ext x
[GOAL]
case H
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ ↑(mapEquiv f (Equiv.refl α)) x = ↑(Equiv.refl (f α)) x
[PROOFSTEP]
simp only [mapEquiv_apply, refl_apply]
[GOAL]
case H
α β : Type u
f : Type u → Type v
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
x : f α
⊢ ↑(Equiv.refl α) <$> x = x
[PROOFSTEP]
exact LawfulFunctor.id_map x
[GOAL]
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
h : α ≃ β
h' : α' ≃ β'
x : F α α'
⊢ bimap (↑h.symm) (↑h'.symm) (bimap (↑h) (↑h') x) = x
[PROOFSTEP]
simp [bimap_bimap, id_bimap]
[GOAL]
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
h : α ≃ β
h' : α' ≃ β'
x : F β β'
⊢ bimap (↑h) (↑h') (bimap (↑h.symm) (↑h'.symm) x) = x
[PROOFSTEP]
simp [bimap_bimap, id_bimap]
[GOAL]
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
⊢ mapEquiv F (Equiv.refl α) (Equiv.refl α') = Equiv.refl (F α α')
[PROOFSTEP]
ext x
[GOAL]
case H
α β : Type u
α' β' : Type v
F : Type u → Type v → Type w
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
x : F α α'
⊢ ↑(mapEquiv F (Equiv.refl α) (Equiv.refl α')) x = ↑(Equiv.refl (F α α')) x
[PROOFSTEP]
simp [id_bimap]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f fab : α → β
fbc : β → γ
ga ga' : α → α
gb gb' : β → β
gc gc' : γ → γ
h : Semiconj f ga gb
h' : Semiconj f ga' gb'
x : α
⊢ f ((ga ∘ ga') x) = (gb ∘ gb') (f x)
[PROOFSTEP]
simp only [comp_apply, h.eq, h'.eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f fab : α → β
fbc : β → γ
ga ga' : α → α
gb gb' : β → β
gc gc' : γ → γ
hab : Semiconj fab ga gb
hbc : Semiconj fbc gb gc
x : α
⊢ (fbc ∘ fab) (ga x) = gc ((fbc ∘ fab) x)
[PROOFSTEP]
simp only [comp_apply, hab.eq, hbc.eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f fab : α → β
fbc : β → γ
ga ga' : α → α
gb gb' : β → β
gc gc' : γ → γ
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
⊢ f (ga' x) = gb' (f x)
[PROOFSTEP]
rw [← hb (f (ga' x)), ← h.eq, ha x]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
f' : β → γ
gc : γ → γ → γ
hf' : Semiconj₂ f' gb gc
hf : Semiconj₂ f ga gb
x y : α
⊢ (f' ∘ f) (ga x y) = gc ((f' ∘ f) x) ((f' ∘ f) y)
[PROOFSTEP]
simp only [hf'.eq, hf.eq, comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : IsAssociative α ga
h : Semiconj₂ f ga gb
h_surj : Surjective f
x₁ x₂ x₃ : α
⊢ gb (gb (f x₁) (f x₂)) (f x₃) = gb (f x₁) (gb (f x₂) (f x₃))
[PROOFSTEP]
simp only [← h.eq, @IsAssociative.assoc _ ga]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : IsAssociative β gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x₁ x₂ x₃ : α
⊢ f (ga (ga x₁ x₂) x₃) = f (ga x₁ (ga x₂ x₃))
[PROOFSTEP]
simp only [h.eq, @IsAssociative.assoc _ gb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : IsIdempotent α ga
h : Semiconj₂ f ga gb
h_surj : Surjective f
x : α
⊢ gb (f x) (f x) = f x
[PROOFSTEP]
simp only [← h.eq, @IsIdempotent.idempotent _ ga]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : IsIdempotent β gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
⊢ f (ga x x) = f x
[PROOFSTEP]
rw [h.eq, @IsIdempotent.idempotent _ gb]