case h.h.a
M : Type u_1
N : Type ?u.20259
P : Type ?u.20262
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
x✝¹ x✝ : M
⊢ ↑(sInf S) x✝¹ x✝ ↔ sInf (FunLike.coe '' S) x✝¹ x✝
M : Type u_1
N : Type ?u.20259
P : Type ?u.20262
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ ↑(sInf S) = sInf (FunLike.coe '' S)
ext
case h.h.a
M : Type u_1
N : Type ?u.20259
P : Type ?u.20262
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
x✝¹ x✝ : M
⊢ ↑(sInf S) x✝¹ x✝ ↔ ∀ (i : Con M), i ∈ S → ↑i x✝¹ x✝
case h.h.a
M : Type u_1
N : Type ?u.20259
P : Type ?u.20262
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
x✝¹ x✝ : M
⊢ ↑(sInf S) x✝¹ x✝ ↔ sInf (FunLike.coe '' S) x✝¹ x✝
simp only [sInf_image, iInf_apply, iInf_Prop_eq]
no goals
case h.h.a
M : Type u_1
N : Type ?u.20259
P : Type ?u.20262
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
x✝¹ x✝ : M
⊢ ↑(sInf S) x✝¹ x✝ ↔ ∀ (i : Con M), i ∈ S → ↑i x✝¹ x✝
rfl