case intro.intro
α : Type u_1
β : Type u_2
σ : Type ?u.29812
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred p
α : Type u_1
β : Type u_2
σ : Type ?u.29812
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
q : β → Prop
h₁ : p ≤₀ q
h₂ : ComputablePred q
⊢ ComputablePred p
rcases h₁ with ⟨f, c, hf⟩
case intro.intro
α : Type u_1
β : Type u_2
σ : Type ?u.29812
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred fun a => q (f a)
case intro.intro
α : Type u_1
β : Type u_2
σ : Type ?u.29812
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred p
rw [show p = fun a => q (f a) from Set.ext hf]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
σ : Type ?u.29812
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a => g a = true
hf : ∀ (a : α), p a ↔ (fun a => g a = true) (f a)
⊢ ComputablePred fun a => (fun a => g a = true) (f a)
case intro.intro
α : Type u_1
β : Type u_2
σ : Type ?u.29812
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred fun a => q (f a)
rcases computable_iff.1 h₂ with ⟨g, hg, rfl⟩
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
σ : Type ?u.29812
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a => g a = true
hf : ∀ (a : α), p a ↔ (fun a => g a = true) (f a)
⊢ ComputablePred fun a => (fun a => g a = true) (f a)
exact ⟨by infer_instance, by simpa using hg.comp c⟩
no goals
α : Type u_1
β : Type u_2
σ : Type ?u.29812
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a => g a = true
hf : ∀ (a : α), p a ↔ (fun a => g a = true) (f a)
⊢ DecidablePred fun a => (fun a => g a = true) (f a)
infer_instance
no goals
α : Type u_1
β : Type u_2
σ : Type ?u.29812
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun a => g a = true
hf : ∀ (a : α), p a ↔ (fun a => g a = true) (f a)
⊢ Computable fun a => decide ((fun a => (fun a => g a = true) (f a)) a)
simpa using hg.comp c