case mp.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ ∃ u, q u

case mpr.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ ∃ u, P u
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
⊢ (∃ u, P u) ↔ ∃ u, q u
constructor <;> rintro ⟨u, h₂⟩
case mp.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ q (f <$$> u)
case mp.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ ∃ u, q u
refine ⟨f <$$> u, ?_⟩
no goals
case mp.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ q (f <$$> u)
apply (h₁ u).mp h₂
case mpr.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ P (g <$$> u)
case mpr.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ ∃ u, P u
refine ⟨g <$$> u, ?_⟩
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ q (f <$$> g <$$> u)
case mpr.intro
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ P (g <$$> u)
apply (h₁ _).mpr _
no goals
n : ℕ
α β γ : TypeVec n
F : TypeVec n → Type v
inst✝¹ : MvFunctor F
P✝ : α ⟹ TypeVec.repeat n Prop
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ q (f <$$> g <$$> u)
simp only [MvFunctor.map_map, h₀, LawfulMvFunctor.id_map, h₂]