α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort ?u.43083
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ (x : { i // p i }), f ↑x (_ : p ↑x)) = ⨅ (x : { i // p i }), l (f ↑x (_ : p ↑x))
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort ?u.43083
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ (i : ι) (hi : p i), f i hi) = ⨅ (i : ι) (hi : p i), l (f i hi)
rw [iInf_subtype', iInf_subtype']
no goals
α : Type u
β : Type v
γ : Type w
ι✝ : Sort x
κ : ι✝ → Sort ?u.43083
a a₁ a₂ : α
b b₁ b₂ : β
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ (x : { i // p i }), f ↑x (_ : p ↑x)) = ⨅ (x : { i // p i }), l (f ↑x (_ : p ↑x))
exact gi.l_iInf_of_ul_eq_self _ fun _ => hf _ _